Working Pattern refactor
authorJoachim Breitner <mail@joachim-breitner.de>
Tue, 31 Aug 2010 09:33:18 +0000 (11:33 +0200)
committerJoachim Breitner <mail@joachim-breitner.de>
Tue, 31 Aug 2010 09:33:18 +0000 (11:33 +0200)
CFGraph/Eval.thy

index ee507b5..4e75111 100644 (file)
@@ -39,8 +39,8 @@ function (sequential,tailrec,domintros)
           = (      let b' = Suc b
                    in if v \<noteq> 0 then evalF contt [] ve b'
                                else evalF contt [] ve b')"
-  |     "evalF Stop [DI i] _ _
-          = (i)"
+  |     "evalF Stop as _ _
+          = (case as of [DI i] \<Rightarrow> i)"
 
   |     "evalC (App lab f vs) \<beta> ve b
           = (let f' = evalV f \<beta> ve;