Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/inductive_realizer.ML
changeset 46708 b138dee7bed3
parent 46219 426ed18eba43
child 47060 e2741ec9ae36 
--- a/src/HOL/Tools/inductive_realizer.ML	Mon Feb 27 15:42:07 2012 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Mon Feb 27 15:48:02 2012 +0100
@@ -456,7 +456,7 @@
         val rews = map mk_meta_eq case_thms;
         val thm = Goal.prove_global thy []
           (Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') (fn {prems, ...} => EVERY
-          [cut_facts_tac [hd prems] 1,
+          [cut_tac (hd prems) 1,
            etac elimR 1,
            ALLGOALS (asm_simp_tac HOL_basic_ss),
            rewrite_goals_tac rews,
isabelle