diff -r 1b3115d1a8df -r 8d8c70b41bab src/HOL/Modelcheck/mucke_oracle.ML
--- a/src/HOL/Modelcheck/mucke_oracle.ML	Thu Mar 03 09:22:35 2005 +0100
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Thu Mar 03 12:43:01 2005 +0100
@@ -96,7 +96,7 @@
 
 fun if_full_simp_tac sset i state =
 let val sign = #sign (rep_thm state);
-        val (subgoal::_) = drop(i-1,prems_of state);
+        val (subgoal::_) = Library.drop(i-1,prems_of state);
         val prems = Logic.strip_imp_prems subgoal;
 	val concl = Logic.strip_imp_concl subgoal;
 	val prems = prems @ [concl];
@@ -253,10 +253,10 @@
       fun newName (Var(ix,_), (pairs,used)) = 
           let val v = variant used (string_of_indexname ix)
           in  ((ix,v)::pairs, v::used)  end;
-      val (alist, _) = foldr newName (vars, ([], used));
+      val (alist, _) = Library.foldr newName (vars, ([], used));
       fun mk_inst (Var(v,T)) = 
           (Var(v,T),
-           Free(the (assoc(alist,v)), T));
+           Free(valOf (assoc(alist,v)), T));
       val insts = map mk_inst vars;
   in subst_atomic insts t end;