src/Pure/Isar/rule_insts.ML

--- a/src/Pure/Isar/rule_insts.ML	Fri Oct 30 18:33:21 2009 +0100
+++ b/src/Pure/Isar/rule_insts.ML	Sun Nov 01 15:24:45 2009 +0100
@@ -177,7 +177,7 @@
         else
           T.assign (SOME (T.Term (the (AList.lookup (op =) term_insts xi)))) arg);
   in
-    Drule.instantiate insts thm |> RuleCases.save thm
+    Drule.instantiate insts thm |> Rule_Cases.save thm
   end;
 
 fun read_instantiate_mixed' ctxt (args, concl_args) thm =