src/HOL/Import/proof_kernel.ML

--- a/src/HOL/Import/proof_kernel.ML	Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Import/proof_kernel.ML	Fri Mar 04 15:07:34 2005 +0100
@@ -675,7 +675,7 @@
 		val (c,asl) = case terms of
 				  [] => raise ERR "x2p" "Bad oracle description"
 				| (hd::tl) => (hd,tl)
-		val tg = Library.foldr (fn (oracle,tg) => Tag.merge (Tag.read oracle) tg) (ors,Tag.empty_tag)
+		val tg = foldr (fn (oracle,tg) => Tag.merge (Tag.read oracle) tg) Tag.empty_tag ors
 	    in
 		mk_proof (POracle(tg,map xml_to_term asl,xml_to_term c))
 	    end
@@ -1064,7 +1064,7 @@
 	  | process _ = raise ERR "disamb_helper" "Internal error"
 
 	val (vars',rens',inst) =
-	    Library.foldr process (varstm,(vars,rens,[]))
+	    foldr process (vars,rens,[]) varstm
     in
 	({vars=vars',rens=rens'},inst)
     end
@@ -1100,22 +1100,22 @@
     end
 
 fun disamb_terms_from info tms =
-    Library.foldr (fn (tm,(info,tms)) =>
+    foldr (fn (tm,(info,tms)) =>
 	      let
 		  val (info',tm') = disamb_term_from info tm
 	      in
 		  (info',tm'::tms)
 	      end)
-	  (tms,(info,[]))
+	  (info,[]) tms
 
 fun disamb_thms_from info hthms =
-    Library.foldr (fn (hthm,(info,thms)) =>
+    foldr (fn (hthm,(info,thms)) =>
 	      let
 		  val (info',tm') = disamb_thm_from info hthm
 	      in
 		  (info',tm'::thms)
 	      end)
-	  (hthms,(info,[]))
+	  (info,[]) hthms
 
 fun disamb_term tm   = disamb_term_from disamb_info_empty tm
 fun disamb_terms tms = disamb_terms_from disamb_info_empty tms
@@ -1127,7 +1127,7 @@
     let
 	val vars = collect_vars (prop_of th)
 	val (rens',inst,_) =
-	    Library.foldr (fn((ren as (vold as Free(vname,_),vnew)),
+	    foldr (fn((ren as (vold as Free(vname,_),vnew)),
 		      (rens,inst,vars)) =>
 		     (case Library.find_first (fn Free(v,_) => v = vname | _ => false) vars of
 			  SOME v' => if v' = vold
@@ -1135,7 +1135,7 @@
 				     else (ren::rens,(vold,vnew)::inst,vnew::vars)
 			| NONE => (rens,(vnew,vold)::inst,vold::vars))
 		   | _ => raise ERR "norm_hthm" "Internal error")
-		  (rens,([],[],vars))
+		  ([],[],vars) rens
 	val (dom,rng) = ListPair.unzip inst
 	val th' = mk_INST (map (cterm_of sg) dom) (map (cterm_of sg) rng) th
 	val nvars = collect_vars (prop_of th')
@@ -1794,7 +1794,7 @@
 		      | inst_type ty1 ty2 (ty as Type(name,tys)) =
 			Type(name,map (inst_type ty1 ty2) tys)
 		in
-		    Library.foldr (fn (v,th) =>
+		    foldr (fn (v,th) =>
 			      let
 				  val cdom = fst (dom_rng (fst (dom_rng cty)))
 				  val vty  = type_of v
@@ -1802,11 +1802,11 @@
 				  val cc = cterm_of sg (Const(cname,newcty))
 			      in
 				  mk_COMB (mk_REFL cc) (mk_ABS v th sg) sg
-			      end) (vlist',th)
+			      end) th vlist'
 		end
 	      | SOME _ => raise ERR "GEN_ABS" "Bad constant"
 	      | NONE => 
-		Library.foldr (fn (v,th) => mk_ABS v th sg) (vlist',th)
+		foldr (fn (v,th) => mk_ABS v th sg) th vlist'
 	val res = HOLThm(rens_of info',th1)
 	val _ = message "RESULT:"
 	val _ = if_debug pth res
@@ -1970,8 +1970,8 @@
 			       Theory.add_consts_i consts thy'
 			   end
 
-	    val thy1 = Library.foldr (fn(name,thy)=>
-				snd (get_defname thyname name thy)) (names,thy1)
+	    val thy1 = foldr (fn(name,thy)=>
+				snd (get_defname thyname name thy)) thy1 names
 	    fun new_name name = fst (get_defname thyname name thy1)
 	    val (thy',res) = SpecificationPackage.add_specification_i NONE
 				 (map (fn name => (new_name name,name,false)) names)
@@ -1989,12 +1989,12 @@
 		     then quotename name
 		     else (quotename newname) ^ ": " ^ (quotename name),thy')
 		end
-	    val (new_names,thy') = Library.foldr (fn(name,(names,thy)) =>
+	    val (new_names,thy') = foldr (fn(name,(names,thy)) =>
 					    let
 						val (name',thy') = handle_const (name,thy)
 					    in
 						(name'::names,thy')
-					    end) (names,([],thy'))
+					    end) ([],thy') names
 	    val thy'' = add_dump ("specification (" ^ (spaces new_names) ^ ") " ^ thmname ^ ": " ^ (smart_string_of_thm th) ^
 				  "\n  by (import " ^ thyname ^ " " ^ thmname ^ ")")
 				 thy'