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 74563 042041c0ebeb
parent 67149 e61557884799 
--- a/src/Tools/induct_tacs.ML	Wed Oct 20 20:04:28 2021 +0200
+++ b/src/Tools/induct_tacs.ML	Wed Oct 20 20:25:33 2021 +0200
@@ -122,14 +122,14 @@
 
 val varss =
   Parse.and_list'
-    (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.embedded_inner_syntax))));
+    (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Parse.embedded_inner_syntax))));
 
 in
 
 val _ =
   Theory.setup
    (Method.setup \<^binding>\<open>case_tac\<close>
-      (Args.goal_spec -- Scan.lift (Args.embedded_inner_syntax -- Parse.for_fixes) -- opt_rule >>
+      (Args.goal_spec -- Scan.lift (Parse.embedded_inner_syntax -- Parse.for_fixes) -- opt_rule >>
         (fn ((quant, (s, xs)), r) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s xs r)))
       "unstructured case analysis on types" #>
     Method.setup \<^binding>\<open>induct_tac\<close>
isabelle