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/Tools/induct_tacs.ML
changeset 54742 7a86358a3c0b
parent 48992 0518bf89c777
child 55111 5792f5106c40 
--- a/src/Tools/induct_tacs.ML	Fri Dec 13 23:53:02 2013 +0100
+++ b/src/Tools/induct_tacs.ML	Sat Dec 14 17:28:05 2013 +0100
@@ -98,7 +98,7 @@
             (_, rule) :: _ => rule
           | [] => raise THM ("No induction rules", 0, [])));
 
-    val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 Object_Logic.atomize);
+    val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 (Object_Logic.atomize ctxt));
     val _ = Method.trace ctxt [rule'];
 
     val concls = Logic.dest_conjunctions (Thm.concl_of rule);
isabelle