Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
cases_tactic;
authorwenzelm
Tue, 22 Nov 2005 19:34:48 +0100
changeset 18228 628c11780077
parent 18227 d4cfa0fee007
child 18229 e5a624483a23
cases_tactic;
src/Pure/Isar/proof.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/proof.ML	Tue Nov 22 19:34:47 2005 +0100
+++ b/src/Pure/Isar/proof.ML	Tue Nov 22 19:34:48 2005 +0100
@@ -386,7 +386,7 @@
 fun no_goal_cases st = map (rpair NONE) (goals st);
 
 fun goal_cases st =
-  RuleCases.make true NONE (Thm.theory_of_thm st, Thm.prop_of st) (goals st);
+  RuleCases.make true NONE (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st));
 
 fun check_theory thy state =
   if subthy (thy, theory_of state) then state
@@ -397,7 +397,7 @@
     val (goal_ctxt, (_, {statement, using, goal, before_qed, after_qed})) = find_goal state;
     val meth = meth_fun (if current_context then context_of state else goal_ctxt);
   in
-    Method.apply meth using goal |> Seq.map (fn (goal', meth_cases) =>
+    Method.apply meth using goal |> Seq.map (fn (meth_cases, goal') =>
       state
       |> check_theory (Thm.theory_of_thm goal')
       |> map_goal
isabelle