src/Pure/Isar/rule_insts.ML
changeset 33368 b1cf34f1855c
parent 33317 b4534348b8fd
child 36950 75b8f26f2f07
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Fri Oct 30 18:33:21 2009 +0100
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Sun Nov 01 15:24:45 2009 +0100
     1.3 @@ -177,7 +177,7 @@
     1.4          else
     1.5            T.assign (SOME (T.Term (the (AList.lookup (op =) term_insts xi)))) arg);
     1.6    in
     1.7 -    Drule.instantiate insts thm |> RuleCases.save thm
     1.8 +    Drule.instantiate insts thm |> Rule_Cases.save thm
     1.9    end;
    1.10  
    1.11  fun read_instantiate_mixed' ctxt (args, concl_args) thm =