src/Pure/Isar/rule_insts.ML
changeset 30510 4120fc59dd85
parent 29606 fedb8be05f24
child 30515 bca05b17b618
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Fri Mar 13 19:53:09 2009 +0100
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Fri Mar 13 19:58:26 2009 +0100
     1.3 @@ -387,9 +387,9 @@
     1.4  local
     1.5  
     1.6  fun gen_inst _ tac _ (quant, ([], thms)) =
     1.7 -      Method.METHOD (fn facts => quant (Method.insert_tac facts THEN' tac thms))
     1.8 +      METHOD (fn facts => quant (Method.insert_tac facts THEN' tac thms))
     1.9    | gen_inst inst_tac _ ctxt (quant, (insts, [thm])) =
    1.10 -      Method.METHOD (fn facts =>
    1.11 +      METHOD (fn facts =>
    1.12          quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm))
    1.13    | gen_inst _ _ _ _ = error "Cannot have instantiations with multiple rules";
    1.14