src/FOL/FOL.thy
changeset 63120 629a4c5e953e
parent 62020 5d208fd2507d
child 69590 e65314985426
     1.1 --- a/src/FOL/FOL.thy	Mon May 23 20:45:10 2016 +0200
     1.2 +++ b/src/FOL/FOL.thy	Mon May 23 21:30:30 2016 +0200
     1.3 @@ -72,7 +72,7 @@
     1.4  \<close>
     1.5  
     1.6  method_setup case_tac = \<open>
     1.7 -  Args.goal_spec -- Scan.lift (Args.name_inner_syntax -- Parse.for_fixes) >>
     1.8 +  Args.goal_spec -- Scan.lift (Args.embedded_inner_syntax -- Parse.for_fixes) >>
     1.9      (fn (quant, (s, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s fixes))
    1.10  \<close> "case_tac emulation (dynamic instantiation!)"
    1.11