src/Pure/Isar/rule_insts.ML
changeset 21879 a3efbae45735
parent 21500 146938537ddc
child 22681 9d42e5365ad1
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Mon Dec 18 08:21:34 2006 +0100
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Mon Dec 18 08:21:35 2006 +0100
     1.3 @@ -349,7 +349,7 @@
     1.4        Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
     1.5  
     1.6  fun inst_args f src ctxt =
     1.7 -  f ctxt (#2 (Method.syntax (Args.goal_spec HEADGOAL -- insts) src ctxt));
     1.8 +  f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts) src ctxt));
     1.9  
    1.10  val insts_var =
    1.11    Scan.optional
    1.12 @@ -357,7 +357,7 @@
    1.13        Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
    1.14  
    1.15  fun inst_args_var f src ctxt =
    1.16 -  f ctxt (#2 (Method.syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt));
    1.17 +  f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt));
    1.18  
    1.19  
    1.20  (* setup *)