src/HOL/Nominal/nominal_induct.ML
changeset 21879 a3efbae45735
parent 20998 714a08286899
child 22072 aabbf8c4de80
     1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Mon Dec 18 08:21:34 2006 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Mon Dec 18 08:21:35 2006 +0100
     1.3 @@ -154,7 +154,7 @@
     1.4    Method.syntax
     1.5     (Args.and_list (Scan.repeat (unless_more_args def_inst)) --
     1.6      avoiding -- fixing -- rule_spec) src
     1.7 -  #> (fn (ctxt, (((x, y), z), w)) =>
     1.8 +  #> (fn ((((x, y), z), w), ctxt) =>
     1.9      Method.RAW_METHOD_CASES (fn facts =>
    1.10        HEADGOAL (nominal_induct_tac ctxt x y z w facts)));
    1.11