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 60695 757549b4bbe6
parent 59830 96008563bfee
child 63120 629a4c5e953e 
--- a/src/Tools/induct_tacs.ML	Wed Jul 08 15:37:32 2015 +0200
+++ b/src/Tools/induct_tacs.ML	Wed Jul 08 19:28:43 2015 +0200
@@ -68,7 +68,7 @@
   let
     val goal = Thm.cprem_of st i;
     val (_, goal_ctxt) = Rule_Insts.goal_context (Thm.term_of goal) ctxt
-    and ((_, goal'), _) = Variable.focus_cterm goal ctxt;
+    and ((_, goal'), _) = Variable.focus_cterm NONE goal ctxt;
     val (prems, concl) = Logic.strip_horn (Thm.term_of goal');
 
     fun induct_var name =
isabelle