# HG changeset patch
# User wenzelm
# Date 1121362104 -7200
# Node ID 5979c46853d1f9f936d1f180ce72a4de577ef22a
# Parent  228d663cc9b350e05063542c433e833c2ef3eb15
tuned;

diff -r 228d663cc9b3 -r 5979c46853d1 src/HOLCF/adm_tac.ML
--- a/src/HOLCF/adm_tac.ML	Thu Jul 14 19:28:23 2005 +0200
+++ b/src/HOLCF/adm_tac.ML	Thu Jul 14 19:28:24 2005 +0200
@@ -80,9 +80,9 @@
 
 
 (*figure out internal names*)
-val chfin_pcpoS = Sign.intern_sort (sign_of HOLCF.thy) ["chfin", "pcpo"];
-val cont_name = Sign.intern_const (sign_of HOLCF.thy) "cont";
-val adm_name = Sign.intern_const (sign_of HOLCF.thy) "adm";
+val chfin_pcpoS = Sign.intern_sort (the_context ()) ["chfin", "pcpo"];
+val cont_name = Sign.intern_const (the_context ()) "cont";
+val adm_name = Sign.intern_const (the_context ()) "adm";
 
 
 (*** check whether type of terms in list is chain finite ***)
diff -r 228d663cc9b3 -r 5979c46853d1 src/HOLCF/cont_consts.ML
--- a/src/HOLCF/cont_consts.ML	Thu Jul 14 19:28:23 2005 +0200
+++ b/src/HOLCF/cont_consts.ML	Thu Jul 14 19:28:24 2005 +0200
@@ -80,7 +80,7 @@
 
 fun gen_add_consts prep_typ raw_decls thy =
   let
-    val decls = map (upd_second (Thm.typ_of o prep_typ (Theory.sign_of thy))) raw_decls;
+    val decls = map (upd_second (Thm.typ_of o prep_typ thy)) raw_decls;
     val (contconst_decls, normal_decls) = List.partition is_contconst decls;
     val transformed_decls = map transform contconst_decls;
   in
diff -r 228d663cc9b3 -r 5979c46853d1 src/HOLCF/domain/axioms.ML
--- a/src/HOLCF/domain/axioms.ML	Thu Jul 14 19:28:23 2005 +0200
+++ b/src/HOLCF/domain/axioms.ML	Thu Jul 14 19:28:24 2005 +0200
@@ -35,7 +35,7 @@
 				Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons));
 
   fun con_def outer recu m n (_,args) = let
-     fun idxs z x arg = (if is_lazy arg then fn t => %%:upN`t else Id)
+     fun idxs z x arg = (if is_lazy arg then fn t => %%:upN`t else I)
 			(if recu andalso is_rec arg then (cproj (Bound z) eqs
 				  (rec_of arg))`Bound(z-x) else Bound(z-x));
      fun parms [] = %%:ONE_N
@@ -47,7 +47,7 @@
 
   val copy_def = ("copy_def", %%:(dname^"_copy") == /\"f" (dc_abs oo 
 	Library.foldl (op `) (%%:(dname^"_when") , 
-	              mapn (con_def Id true (length cons)) 0 cons)));
+	              mapn (con_def I true (length cons)) 0 cons)));
 
 (* -- definitions concerning the constructors, discriminators and selectors - *)
 
@@ -75,7 +75,7 @@
 		 mk_cRep_CFun(%%:(dname^"_when"),map 
 			(fn (con',args) => if con'<>con then UU else
 			 foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg);
-	in List.mapPartial Id (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end;
+	in List.mapPartial I (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end;
 
 
 (* ----- axiom and definitions concerning induction ------------------------- *)
diff -r 228d663cc9b3 -r 5979c46853d1 src/HOLCF/domain/library.ML
--- a/src/HOLCF/domain/library.ML	Thu Jul 14 19:28:23 2005 +0200
+++ b/src/HOLCF/domain/library.ML	Thu Jul 14 19:28:24 2005 +0200
@@ -8,8 +8,6 @@
 
 (* ----- general support ---------------------------------------------------- *)
 
-fun Id x = x;
-
 fun mapn f n []      = []
 |   mapn f n (x::xs) = (f n x) :: mapn f (n+1) xs;
 
@@ -17,7 +15,7 @@
 			     | itr [a] = f2 a
 			     | itr (a::l) = f(a, itr l)
 in  itr l  end;
-fun foldr' f l = foldr'' f (l,Id);
+fun foldr' f l = foldr'' f (l,I);
 fun map_cumulr f start xs = foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) =>
 						  (y::ys,res2)) ([],start) xs;
 
@@ -175,9 +173,9 @@
 infixr 0 ==>;   fun S ==> T = mk_trp S ===> mk_trp T;
 infix 0 ==;     fun S ==  T = %%:"==" $ S $ T;
 infix 1 ===;    fun S === T = %%:"op =" $ S $ T;
-infix 1 ~=;     fun S ~=  T = mk_not (S === T);
+infix 1 ~=;     fun S ~=  T = HOLogic.mk_not (S === T);
 infix 1 <<;     fun S <<  T = %%:lessN $ S $ T;
-infix 1 ~<<;    fun S ~<< T = mk_not (S << T);
+infix 1 ~<<;    fun S ~<< T = HOLogic.mk_not (S << T);
 
 infix 9 `  ; fun f`  x = %%:Rep_CFunN $ f $ x;
 infix 9 `% ; fun f`% s = f` %: s;
@@ -186,7 +184,7 @@
 fun con_app2 con f args = mk_cRep_CFun(%%:con,map f args);
 fun con_app con = con_app2 con %#;
 fun if_rec  arg f y   = if is_rec arg then f (rec_of arg) else y;
-fun app_rec_arg p arg = if_rec arg (fn n => fn x => (p n)`x) Id (%# arg);
+fun app_rec_arg p arg = if_rec arg (fn n => fn x => (p n)`x) I (%# arg);
 fun prj _  _  x (   _::[]) _ = x
 |   prj f1 _  x (_::y::ys) 0 = f1 x y
 |   prj f1 f2 x (y::   ys) j = prj f1 f2 (f2 x y) ys (j-1);
@@ -195,11 +193,11 @@
 fun  proj x      = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x;
 fun cproj x      = prj (fn S => K(%%:cfstN`S)) (fn S => K(%%:csndN`S)) x;
 fun prj' _  _  x (   _::[]) _ = x
-|   prj' f1 _  x (_::   ys) 0 = f1 x (foldr' mk_prodT ys)
+|   prj' f1 _  x (_::   ys) 0 = f1 x (foldr' HOLogic.mk_prodT ys)
 |   prj' f1 f2 x (y::   ys) j = prj' f1 f2 (f2 x y) ys (j-1);
 fun cproj' T eqs = prj'
-	(fn S => fn t => Const(cfstN,mk_prodT(dummyT,t)->>dummyT)`S)
-	(fn S => fn t => Const(csndN,mk_prodT(t,dummyT)->>dummyT)`S) 
+	(fn S => fn t => Const(cfstN, HOLogic.mk_prodT(dummyT,t)->>dummyT)`S)
+	(fn S => fn t => Const(csndN, HOLogic.mk_prodT(t,dummyT)->>dummyT)`S) 
 		       T (map ((fn tp => tp ->> tp) o Type o fix_tp o fst) eqs);
 fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
 
@@ -215,7 +213,7 @@
 |   mk_ctuple (t::ts) = cpair (t, mk_ctuple ts);
 fun mk_ctupleT [] = HOLogic.unitT   (* used in match_defs *)
 |   mk_ctupleT (T::[]) = T
-|   mk_ctupleT (T::Ts) = mk_prodT(T, mk_ctupleT Ts);
+|   mk_ctupleT (T::Ts) = HOLogic.mk_prodT(T, mk_ctupleT Ts);
 fun lift_defined f = lift (fn x => defined (f x));
 fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1);
 
@@ -236,13 +234,13 @@
 	|   one_fun n (_,args) = let
 		val l2 = length args;
 		fun idxs m arg = (if is_lazy arg then fn x=> %%:fupN` %%:ID_N`x
-					         else Id) (Bound(l2-m));
+					         else I) (Bound(l2-m));
 		in cont_eta_contract (foldr'' 
 			(fn (a,t) => %%:ssplitN`(/\# (a,t)))
 			(args,
 			fn a=> /\#(a,(mk_cRep_CFun(funarg(l2,n),mapn idxs 1 args))))
 			) end;
 in (if length cons = 1 andalso length(snd(hd cons)) <= 1
-    then fn t => %%:strictifyN`t else Id)
+    then fn t => %%:strictifyN`t else I)
      (foldr' (fn (x,y)=> %%:sscaseN`x`y) (mapn one_fun 1 cons)) end;
 end; (* struct *)
diff -r 228d663cc9b3 -r 5979c46853d1 src/HOLCF/domain/syntax.ML
--- a/src/HOLCF/domain/syntax.ML	Thu Jul 14 19:28:23 2005 +0200
+++ b/src/HOLCF/domain/syntax.ML	Thu Jul 14 19:28:24 2005 +0200
@@ -105,8 +105,8 @@
 let
   val dtypes  = map (Type o fst) eqs';
   val boolT   = HOLogic.boolT;
-  val funprod = foldr' mk_prodT (map (fn tp => tp ->> tp          ) dtypes);
-  val relprod = foldr' mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
+  val funprod = foldr' HOLogic.mk_prodT (map (fn tp => tp ->> tp          ) dtypes);
+  val relprod = foldr' HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
   val const_copy   = (comp_dnam^"_copy"  ,funprod ->> funprod, NoSyn);
   val const_bisim  = (comp_dnam^"_bisim" ,relprod --> boolT  , NoSyn);
   val ctt           = map (calc_syntax funprod) eqs';
diff -r 228d663cc9b3 -r 5979c46853d1 src/HOLCF/domain/theorems.ML
--- a/src/HOLCF/domain/theorems.ML	Thu Jul 14 19:28:23 2005 +0200
+++ b/src/HOLCF/domain/theorems.ML	Thu Jul 14 19:28:24 2005 +0200
@@ -6,6 +6,7 @@
 Proof generator for domain section.
 *)
 
+val HOLCF_ss = simpset();
 
 structure Domain_Theorems = struct
 
@@ -233,7 +234,7 @@
                                                   (List.nth(vns,n))] else [])
                      @ [asm_simp_tac(HOLCF_ss addsimps when_rews)1])end) cons;
 in List.concat(map  (fn (c,args) => 
-     List.concat(List.mapPartial Id (mapn (fn n => fn arg => Option.map (one_sel c n) (sel_of arg)) 0 args))) cons) end;
+     List.concat(List.mapPartial I (mapn (fn n => fn arg => Option.map (one_sel c n) (sel_of arg)) 0 args))) cons) end;
 val sel_defins = if length cons=1 then List.mapPartial (fn arg => Option.map (fn sel => pg [](defined(%:x_name)==> 
                         defined(%%:sel`%x_name)) [
                                 rtac casedist 1,
@@ -442,7 +443,7 @@
     fun all_rec_to ns  = rec_to forall not all_rec_to  ns;
     fun warn (n,cons)  = if all_rec_to [] false (n,cons) then (warning
         ("domain "^List.nth(dnames,n)^" is empty!"); true) else false;
-    fun lazy_rec_to ns = rec_to exists Id  lazy_rec_to ns;
+    fun lazy_rec_to ns = rec_to exists I  lazy_rec_to ns;
 
   in val n__eqs     = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs;
      val is_emptys = map warn n__eqs;
diff -r 228d663cc9b3 -r 5979c46853d1 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Thu Jul 14 19:28:23 2005 +0200
+++ b/src/Pure/Isar/obtain.ML	Thu Jul 14 19:28:24 2005 +0200
@@ -118,11 +118,10 @@
     |> Method.proof (SOME (Method.Basic (K Method.succeed))) |> Seq.hd
     |> Proof.fix_i [([thesisN], NONE)]
     |> Proof.assume_i [((thatN, [ContextRules.intro_query_local NONE]), [(that_prop, ([], []))])]
-    |> (fn state' =>
-        state'
-        |> Proof.from_facts chain_facts
-        |> Proof.show_i (K I) after_qed false [(("", []), [(bound_thesis, ([], []))])] false
-        |> Method.refine (Method.Basic (K (Method.insert (Proof.the_facts state')))))
+    |> `Proof.the_facts
+    ||> Proof.from_facts chain_facts
+    ||> Proof.show_i (K I) after_qed false [(("", []), [(bound_thesis, ([], []))])] false
+    |-> (fn facts => Method.refine (Method.Basic (K (Method.insert facts))))
   end;
 
 val obtain = gen_obtain ProofContext.read_vars ProofContext.read_propp;
diff -r 228d663cc9b3 -r 5979c46853d1 src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Thu Jul 14 19:28:23 2005 +0200
+++ b/src/Pure/Isar/skip_proof.ML	Thu Jul 14 19:28:24 2005 +0200
@@ -41,13 +41,13 @@
 (* basic cheating *)
 
 fun make_thm thy t =
-  Thm.invoke_oracle_i thy "Pure.skip_proof" (Theory.sign_of thy, SkipProof t);
+  Thm.invoke_oracle_i thy "Pure.skip_proof" (thy, SkipProof t);
 
 fun cheat_tac thy st =
   ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
 
 fun prove thy xs asms prop tac =
-  Tactic.prove (Theory.sign_of thy) xs asms prop
+  Tactic.prove thy xs asms prop
     (if ! quick_and_dirty then (K (cheat_tac thy)) else tac);
 
 
diff -r 228d663cc9b3 -r 5979c46853d1 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Jul 14 19:28:23 2005 +0200
+++ b/src/Pure/ROOT.ML	Thu Jul 14 19:28:24 2005 +0200
@@ -1,9 +1,7 @@
 (*  Title:      Pure/ROOT.ML
     ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
 
-Root file for Pure Isabelle.
+Pure Isabelle.
 *)
 
 val banner = "Pure Isabelle";
@@ -93,10 +91,8 @@
 (*configuration for Proof General*)
 use "proof_general.ML";
 
-(* loading the Tools directory *)
 cd "Tools"; use "ROOT.ML"; cd "..";
 
-(*the Pure theories*)
 use_thy "Pure"; structure Pure = struct val thy = theory "Pure" end;
 use_thy "CPure"; structure CPure = struct val thy = theory "CPure" end;
 
diff -r 228d663cc9b3 -r 5979c46853d1 src/Pure/Tools/ROOT.ML
--- a/src/Pure/Tools/ROOT.ML	Thu Jul 14 19:28:23 2005 +0200
+++ b/src/Pure/Tools/ROOT.ML	Thu Jul 14 19:28:24 2005 +0200
@@ -1,8 +1,11 @@
 (*  Title:      Pure/Tools/ROOT.ML
     ID:         $Id$
+
+Miscellaneous tools and packages for Pure Isabelle.
 *)
 
+(*Steven Obua's evaluator*)
 use "am_interpreter.ML";
-use "am_compiler.ML"; 
+use "am_compiler.ML";
 use "am_util.ML";
 use "compute.ML";
diff -r 228d663cc9b3 -r 5979c46853d1 src/Pure/Tools/am_compiler.ML
--- a/src/Pure/Tools/am_compiler.ML	Thu Jul 14 19:28:23 2005 +0200
+++ b/src/Pure/Tools/am_compiler.ML	Thu Jul 14 19:28:24 2005 +0200
@@ -5,14 +5,14 @@
 
 signature COMPILING_AM = 
 sig
-    include ABSTRACT_MACHINE
+  include ABSTRACT_MACHINE
 
-    datatype closure = CVar of int | CConst of int
-		     | CApp of closure * closure | CAbs of closure | Closure of (closure list) * closure
+  datatype closure = CVar of int | CConst of int
+    | CApp of closure * closure | CAbs of closure | Closure of (closure list) * closure
 
-    val set_compiled_rewriter : (term -> closure) -> unit
-    val list_nth : 'a list * int -> 'a
-    val list_map : ('a -> 'b) -> 'a list -> 'b list
+  val set_compiled_rewriter : (term -> closure) -> unit
+  val list_nth : 'a list * int -> 'a
+  val list_map : ('a -> 'b) -> 'a list -> 'b list
 end
 
 structure AM_Compiler :> COMPILING_AM = struct
@@ -25,7 +25,8 @@
 datatype pattern = PVar | PConst of int * (pattern list)
 
 datatype closure = CVar of int | CConst of int
-		 | CApp of closure * closure | CAbs of closure | Closure of (closure list) * closure
+	         | CApp of closure * closure | CAbs of closure
+                 | Closure of (closure list) * closure
 
 val compiled_rewriter = ref (NONE:(term -> closure)Option.option)
 
@@ -47,19 +48,22 @@
   | term_of_clos (CConst c) = Const c
   | term_of_clos (CApp (u, v)) = App (term_of_clos u, term_of_clos v)
   | term_of_clos (CAbs u) = Abs (term_of_clos u)
-  | term_of_clos (Closure (e, u)) = raise (Run "internal error: closure in normalized term found")
+  | term_of_clos (Closure (e, u)) =
+      raise (Run "internal error: closure in normalized term found")
 
 fun strip_closure args (CApp (a,b)) = strip_closure (b::args) a
   | strip_closure args x = (x, args)
 
-(* Returns true iff at most 0 .. (free-1) occur unbound. therefore check_freevars 0 t iff t is closed *)
+(*Returns true iff at most 0 .. (free-1) occur unbound. therefore
+  check_freevars 0 t iff t is closed*)
 fun check_freevars free (Var x) = x < free
   | check_freevars free (Const c) = true
   | check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v
   | check_freevars free (Abs m) = check_freevars (free+1) m
 
 fun count_patternvars PVar = 1
-  | count_patternvars (PConst (_, ps)) = List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
+  | count_patternvars (PConst (_, ps)) =
+      List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
 
 fun print_rule (p, t) = 
     let	
@@ -81,17 +85,22 @@
 	    end
 
 	val (n, pattern) = print_pattern 0 p
-	val pattern = if List.exists Char.isSpace (String.explode pattern) then "("^pattern^")" else pattern
+	val pattern =
+            if List.exists Char.isSpace (String.explode pattern) then "("^pattern^")"
+            else pattern
 	
-	fun print_term d (Var x) = (*if x < d then "Var "^(str x) else "x"^(str (n-(x-d)-1))*) "Var "^(str x)
-	  | print_term d (Const c) = "c"^(str c)
-	  | print_term d (App (a,b)) = "App ("^(print_term d a)^", "^(print_term d b)^")"
-	  | print_term d (Abs c) = "Abs ("^(print_term (d+1) c)^")"
+	fun print_term d (Var x) = (*if x < d then "Var "^(str x) else "x"^(str (n-(x-d)-1))*)
+              "Var " ^ str x
+	  | print_term d (Const c) = "c" ^ str c
+	  | print_term d (App (a,b)) = "App (" ^ print_term d a ^ ", " ^ print_term d b ^ ")"
+	  | print_term d (Abs c) = "Abs (" ^ print_term (d + 1) c ^ ")"
 
 	fun listvars n = if n = 0 then "x0" else "x"^(str n)^", "^(listvars (n-1))
 
 	val term = print_term 0 t
-	val term = if n > 0 then "Closure (["^(listvars (n-1))^"], "^term^")" else "Closure ([], "^term^")"
+	val term =
+            if n > 0 then "Closure (["^(listvars (n-1))^"], "^term^")"
+            else "Closure ([], "^term^")"
 			   
     in
 	"lookup stack "^pattern^" = weak stack ("^term^")"
@@ -104,7 +113,7 @@
   | remove_dups [] = []
 
 fun constants_of PVar = []
-  | constants_of (PConst (c, ps)) = c::(List.concat (map constants_of ps))
+  | constants_of (PConst (c, ps)) = c :: List.concat (map constants_of ps)
 
 fun constants_of_term (Var _) = []
   | constants_of_term (Abs m) = constants_of_term m
@@ -113,6 +122,7 @@
     
 fun load_rules sname name prog = 
     let
+        (* FIXME consider using more readable/efficient Buffer.empty |> fold Buffer.add etc. *)
 	val buffer = ref ""
 	fun write s = (buffer := (!buffer)^s)
 	fun writeln s = (write s; write "\n")
@@ -210,11 +220,9 @@
 	    in
 		()
 	    end
-	    
-	val dummy = (fn s => ())		    
     in
 	compiled_rewriter := NONE;	
-	use_text (dummy, dummy) false (!buffer);
+	use_text (K (), K ()) false (!buffer);
 	case !compiled_rewriter of 
 	    NONE => raise (Compile "cannot communicate with compiled function")
 	  | SOME r => (compiled_rewriter := NONE; fn t => term_of_clos (r t))
diff -r 228d663cc9b3 -r 5979c46853d1 src/Pure/Tools/am_interpreter.ML
--- a/src/Pure/Tools/am_interpreter.ML	Thu Jul 14 19:28:23 2005 +0200
+++ b/src/Pure/Tools/am_interpreter.ML	Thu Jul 14 19:28:24 2005 +0200
@@ -3,7 +3,9 @@
     Author:     Steven Obua
 *)
 
-signature ABSTRACT_MACHINE = sig							     
+signature ABSTRACT_MACHINE =
+sig
+
 datatype term = Var of int | Const of int | App of term * term | Abs of term
 
 datatype pattern = PVar | PConst of int * (pattern list)
@@ -12,7 +14,7 @@
 
 exception Compile of string;
 val compile : (pattern * term) list -> program
- 
+
 exception Run of string;
 val run : program -> term -> term
 
@@ -25,8 +27,8 @@
 datatype pattern = PVar | PConst of int * (pattern list)
 
 datatype closure = CVar of int | CConst of int
-		 | CApp of closure * closure | CAbs of closure 
-		 | Closure of (closure list) * closure 
+                 | CApp of closure * closure | CAbs of closure
+                 | Closure of (closure list) * closure
 
 structure prog_struct = TableFun(type key = int*int val ord = prod_ord int_ord int_ord);
 
@@ -57,22 +59,22 @@
 
 (* earlier occurrence of PVar corresponds to higher de Bruijn index *)
 fun pattern_match args PVar clos = SOME (clos::args)
-  | pattern_match args (PConst (c, patterns)) clos = 
+  | pattern_match args (PConst (c, patterns)) clos =
     let
-	val (f, closargs) = strip_closure [] clos
+        val (f, closargs) = strip_closure [] clos
     in
-	case f of 
-	    CConst d => 
-	    if c = d then 
-		pattern_match_list args patterns closargs
-	    else 
-		NONE
-	  | _ => NONE
+        case f of
+            CConst d =>
+            if c = d then
+                pattern_match_list args patterns closargs
+            else
+                NONE
+          | _ => NONE
     end
 and pattern_match_list args [] [] = SOME args
-  | pattern_match_list args (p::ps) (c::cs) = 
+  | pattern_match_list args (p::ps) (c::cs) =
     (case pattern_match args p c of
-	NONE => NONE
+        NONE => NONE
       | SOME args => pattern_match_list args ps cs)
   | pattern_match_list _ _ _ = NONE
 
@@ -88,26 +90,26 @@
 fun pattern_key (PConst (c, ps)) = (c, length ps)
   | pattern_key _ = raise (Compile "pattern reduces to variable")
 
-fun compile eqs = 
+fun compile eqs =
     let
-	val eqs = map (fn (p, r) => (check_freevars (count_patternvars p) r; 
-				     (pattern_key p, (p, clos_of_term r)))) eqs
+        val eqs = map (fn (p, r) => (check_freevars (count_patternvars p) r;
+                                     (pattern_key p, (p, clos_of_term r)))) eqs
     in
-	prog_struct.make (map (fn (k, a) => (k, [a])) eqs)
-    end	
+        prog_struct.make (map (fn (k, a) => (k, [a])) eqs)
+    end
 
 fun match_rules n [] clos = NONE
   | match_rules n ((p,eq)::rs) clos =
     case pattern_match [] p clos of
-	NONE => match_rules (n+1) rs clos
+        NONE => match_rules (n+1) rs clos
       | SOME args => SOME (Closure (args, eq))
 
-fun match_closure prog clos = 
+fun match_closure prog clos =
     case len_head_of_closure 0 clos of
-	(len, CConst c) =>
-	(case prog_struct.lookup (prog, (c, len)) of
-	    NONE => NONE
-	  | SOME rules => match_rules 0 rules clos)
+        (len, CConst c) =>
+        (case prog_struct.lookup (prog, (c, len)) of
+            NONE => NONE
+          | SOME rules => match_rules 0 rules clos)
       | _ => NONE
 
 fun lift n (c as (CConst _)) = c
@@ -121,21 +123,21 @@
   | weak prog (SAppL (b, stack)) (Closure (e, CAbs m)) = weak prog stack (Closure (b::e, m))
   | weak prog stack (Closure (e, CVar n)) = weak prog stack (List.nth (e, n) handle Subscript => (CVar (n-(length e))))
   | weak prog stack (Closure (e, c as CConst _)) = weak prog stack c
-  | weak prog stack clos =    
+  | weak prog stack clos =
     case match_closure prog clos of
-	NONE => weak_last prog stack clos
+        NONE => weak_last prog stack clos
       | SOME r => weak prog stack r
 and weak_last prog (SAppR (a, stack)) b = weak prog stack (CApp (a,b))
   | weak_last prog (s as (SAppL (b, stack))) a = weak prog (SAppR (a, stack)) b
-  | weak_last prog stack c = (stack, c) 
+  | weak_last prog stack c = (stack, c)
 
-fun strong prog stack (Closure (e, CAbs m)) = 
+fun strong prog stack (Closure (e, CAbs m)) =
     let
-	val (stack', wnf) = weak prog SEmpty (Closure ((CVar 0)::(lift_env 0 e), m))
+        val (stack', wnf) = weak prog SEmpty (Closure ((CVar 0)::(lift_env 0 e), m))
     in
-	case stack' of
-	    SEmpty => strong prog (SAbs stack) wnf
-	  | _ => raise (Run "internal error in strong: weak failed")
+        case stack' of
+            SEmpty => strong prog (SAbs stack) wnf
+          | _ => raise (Run "internal error in strong: weak failed")
     end
   | strong prog stack (clos as (CApp (u, v))) = strong prog (SAppL (v, stack)) u
   | strong prog stack clos = strong_last prog stack clos
@@ -144,17 +146,17 @@
   | strong_last prog (SAppR (a, stack)) b = strong_last prog stack (CApp (a, b))
   | strong_last prog stack clos = (stack, clos)
 
-fun run prog t = 
+fun run prog t =
     let
-	val (stack, wnf) = weak prog SEmpty (Closure ([], clos_of_term t))
+        val (stack, wnf) = weak prog SEmpty (Closure ([], clos_of_term t))
     in
-	case stack of 
-	    SEmpty => (case strong prog SEmpty wnf of
-			   (SEmpty, snf) => term_of_clos snf
-			 | _ => raise (Run "internal error in run: strong failed"))
-	  | _ => raise (Run "internal error in run: weak failed")
+        case stack of
+            SEmpty => (case strong prog SEmpty wnf of
+                           (SEmpty, snf) => term_of_clos snf
+                         | _ => raise (Run "internal error in run: strong failed"))
+          | _ => raise (Run "internal error in run: weak failed")
     end
-	  
+
 end
 
 structure AbstractMachine = AM_Interpreter
diff -r 228d663cc9b3 -r 5979c46853d1 src/Pure/Tools/am_util.ML
--- a/src/Pure/Tools/am_util.ML	Thu Jul 14 19:28:23 2005 +0200
+++ b/src/Pure/Tools/am_util.ML	Thu Jul 14 19:28:24 2005 +0200
@@ -4,11 +4,11 @@
 *)
 
 signature AM_UTIL = sig
-    
+
     type naming = string -> int
 
     exception Parse of string
-    exception Tokenize 
+    exception Tokenize
 
     (* takes a naming for the constants *)
     val read_rule : naming -> string -> AbstractMachine.pattern * AbstractMachine.term
@@ -25,7 +25,8 @@
 
 fun term_ord (AbstractMachine.Var x, AbstractMachine.Var y) = int_ord (x,y)
   | term_ord (AbstractMachine.Const c1, AbstractMachine.Const c2) = int_ord (c1, c2)
-  | term_ord (AbstractMachine.App a1, AbstractMachine.App a2) = (prod_ord term_ord term_ord) (a1, a2)
+  | term_ord (AbstractMachine.App a1, AbstractMachine.App a2) =
+      prod_ord term_ord term_ord (a1, a2)
   | term_ord (AbstractMachine.Abs m1, AbstractMachine.Abs m2) = term_ord (m1, m2)
   | term_ord (AbstractMachine.Const _, _) = LESS
   | term_ord (AbstractMachine.Var _, AbstractMachine.Const _ ) = GREATER
@@ -36,68 +37,72 @@
 
 type naming = string -> int
 
-datatype token = TokenConst of string | TokenLeft | TokenRight | TokenVar of string | TokenLambda | TokenDot | TokenNone | TokenEq
+datatype token =
+  TokenConst of string | TokenLeft | TokenRight | TokenVar of string |
+  TokenLambda | TokenDot | TokenNone | TokenEq
 
 exception Tokenize;
 
 fun tokenize s =
     let
-	val s = String.explode s
-	fun str c = Char.toString c
-	fun app s c = s^(str c)
-	fun tz TokenNone [] = []
-	  | tz x [] = [x]
-	  | tz TokenNone (c::cs) = 
-	    if Char.isSpace c then tz TokenNone cs
-	    else if Char.isLower c then (tz (TokenVar (str c)) cs)
-	    else if Char.isAlphaNum c then (tz (TokenConst (str c)) cs)
-	    else if c = #"%" then (TokenLambda :: (tz TokenNone cs))
-	    else if c = #"." then (TokenDot :: (tz TokenNone cs))
-	    else if c = #"(" then (TokenLeft :: (tz TokenNone cs))
-	    else if c = #")" then (TokenRight :: (tz TokenNone cs))
-	    else if c = #"=" then (TokenEq :: (tz TokenNone cs))
-	    else raise Tokenize
-	  | tz (TokenConst s) (c::cs) = 
-	    if Char.isAlphaNum c then (tz (TokenConst (app s c)) cs)
-	    else (TokenConst s)::(tz TokenNone (c::cs))
-	  | tz (TokenVar s) (c::cs) = 
-	    if Char.isAlphaNum c then (tz (TokenVar (app s c)) cs)
-	    else (TokenVar s)::(tz TokenNone (c::cs))
-	  | tz _ _ = raise Tokenize
+        val s = String.explode s
+        fun str c = Char.toString c
+        fun app s c = s^(str c)
+        fun tz TokenNone [] = []
+          | tz x [] = [x]
+          | tz TokenNone (c::cs) =
+            if Char.isSpace c then tz TokenNone cs
+            else if Char.isLower c then (tz (TokenVar (str c)) cs)
+            else if Char.isAlphaNum c then (tz (TokenConst (str c)) cs)
+            else if c = #"%" then (TokenLambda :: (tz TokenNone cs))
+            else if c = #"." then (TokenDot :: (tz TokenNone cs))
+            else if c = #"(" then (TokenLeft :: (tz TokenNone cs))
+            else if c = #")" then (TokenRight :: (tz TokenNone cs))
+            else if c = #"=" then (TokenEq :: (tz TokenNone cs))
+            else raise Tokenize
+          | tz (TokenConst s) (c::cs) =
+            if Char.isAlphaNum c then (tz (TokenConst (app s c)) cs)
+            else (TokenConst s)::(tz TokenNone (c::cs))
+          | tz (TokenVar s) (c::cs) =
+            if Char.isAlphaNum c then (tz (TokenVar (app s c)) cs)
+            else (TokenVar s)::(tz TokenNone (c::cs))
+          | tz _ _ = raise Tokenize
     in
-	tz TokenNone s
+        tz TokenNone s
     end
 
 exception Parse of string;
 
-fun cons x xs = if List.exists (fn y => x = y) xs then raise (Parse ("variable occurs twice: "^x)) else (x::xs)
+fun cons x xs =
+  if List.exists (fn y => x = y) xs then raise (Parse ("variable occurs twice: "^x))
+  else (x::xs)
 
-fun parse_pattern f pvars ((TokenConst c)::ts) = 
+fun parse_pattern f pvars ((TokenConst c)::ts) =
     let
-	val (pvars, ts, plist) = parse_pattern_list f pvars ts
+        val (pvars, ts, plist) = parse_pattern_list f pvars ts
     in
-	(pvars, ts, AbstractMachine.PConst (f c, plist))
+        (pvars, ts, AbstractMachine.PConst (f c, plist))
     end
   | parse_pattern _ _ _ = raise (Parse "parse_pattern: constant expected")
-and parse_pattern_single f pvars ((TokenVar x)::ts) = (cons x pvars, ts, AbstractMachine.PVar)	
+and parse_pattern_single f pvars ((TokenVar x)::ts) = (cons x pvars, ts, AbstractMachine.PVar)
   | parse_pattern_single f pvars ((TokenConst c)::ts) = (pvars, ts, AbstractMachine.PConst (f c, []))
-  | parse_pattern_single f pvars (TokenLeft::ts) = 
+  | parse_pattern_single f pvars (TokenLeft::ts) =
     let
-	val (pvars, ts, p) = parse_pattern f pvars ts
+        val (pvars, ts, p) = parse_pattern f pvars ts
     in
-	case ts of
-	    TokenRight::ts => (pvars, ts, p)
-	  | _ => raise (Parse "parse_pattern_single: closing bracket expected")
+        case ts of
+            TokenRight::ts => (pvars, ts, p)
+          | _ => raise (Parse "parse_pattern_single: closing bracket expected")
     end
   | parse_pattern_single _ _ _ = raise (Parse "parse_pattern_single: got stuck")
 and parse_pattern_list f pvars (TokenEq::ts) = (pvars, TokenEq::ts, [])
   | parse_pattern_list f pvars (TokenRight::ts) = (pvars, TokenRight::ts, [])
-  | parse_pattern_list f pvars ts = 
+  | parse_pattern_list f pvars ts =
     let
-	val (pvars, ts, p) = parse_pattern_single f pvars ts
-	val (pvars, ts, ps) = parse_pattern_list f pvars ts
+        val (pvars, ts, p) = parse_pattern_single f pvars ts
+        val (pvars, ts, ps) = parse_pattern_list f pvars ts
     in
-	(pvars, ts, p::ps)
+        (pvars, ts, p::ps)
     end
 
 fun app_terms x (t::ts) = app_terms (AbstractMachine.App (x, t)) ts
@@ -105,66 +110,66 @@
 
 fun parse_term_single f vars ((TokenConst c)::ts) = (ts, AbstractMachine.Const (f c))
   | parse_term_single f vars ((TokenVar v)::ts) = (ts, AbstractMachine.Var (vars v))
-  | parse_term_single f vars (TokenLeft::ts) = 
+  | parse_term_single f vars (TokenLeft::ts) =
     let
-	val (ts, term) = parse_term f vars ts
+        val (ts, term) = parse_term f vars ts
     in
-	case ts of 
-	    TokenRight::ts => (ts, term)
-	  | _ => raise Parse ("parse_term_single: closing bracket expected")
+        case ts of
+            TokenRight::ts => (ts, term)
+          | _ => raise Parse ("parse_term_single: closing bracket expected")
     end
-  | parse_term_single f vars (TokenLambda::(TokenVar x)::TokenDot::ts) = 
+  | parse_term_single f vars (TokenLambda::(TokenVar x)::TokenDot::ts) =
     let
-	val (ts, term) = parse_term f (fn s => if s=x then 0 else (vars s)+1) ts
+        val (ts, term) = parse_term f (fn s => if s=x then 0 else (vars s)+1) ts
     in
-	(ts, AbstractMachine.Abs term)
+        (ts, AbstractMachine.Abs term)
     end
   | parse_term_single _ _ _ = raise Parse ("parse_term_single: got stuck")
 and parse_term_list f vars [] = ([], [])
   | parse_term_list f vars (TokenRight::ts) = (TokenRight::ts, [])
-  | parse_term_list f vars ts = 
+  | parse_term_list f vars ts =
     let
-	val (ts, term) = parse_term_single f vars ts
-	val (ts, terms) = parse_term_list f vars ts
+        val (ts, term) = parse_term_single f vars ts
+        val (ts, terms) = parse_term_list f vars ts
     in
-	(ts, term::terms)
+        (ts, term::terms)
     end
-and parse_term f vars ts = 
+and parse_term f vars ts =
     let
-	val (ts, terms) = parse_term_list f vars ts
+        val (ts, terms) = parse_term_list f vars ts
     in
-	case terms of 
-	    [] => raise (Parse "parse_term: no term found")
-	  | (t::terms) => (ts, app_terms t terms)
+        case terms of
+            [] => raise (Parse "parse_term: no term found")
+          | (t::terms) => (ts, app_terms t terms)
     end
 
-fun read_rule f s = 
+fun read_rule f s =
     let
-	val t = tokenize s
-	val (v, ts, pattern) = parse_pattern f [] t
-	fun vars [] (x:string) = raise (Parse "read_rule.vars: variable not found")
-	  | vars (v::vs) x = if v = x then 0 else (vars vs x)+1
+        val t = tokenize s
+        val (v, ts, pattern) = parse_pattern f [] t
+        fun vars [] (x:string) = raise (Parse "read_rule.vars: variable not found")
+          | vars (v::vs) x = if v = x then 0 else (vars vs x)+1
     in
-	case ts of 
-	    TokenEq::ts => 
-	    let
-		val (ts, term) = parse_term f (vars v) ts
-	    in
-		case ts of 
-		    [] => (pattern, term)
-		  | _ => raise (Parse "read_rule: still tokens left, end expected")
-	    end
-	  | _ => raise (Parse ("read_rule: = expected"))
+        case ts of
+            TokenEq::ts =>
+            let
+                val (ts, term) = parse_term f (vars v) ts
+            in
+                case ts of
+                    [] => (pattern, term)
+                  | _ => raise (Parse "read_rule: still tokens left, end expected")
+            end
+          | _ => raise (Parse ("read_rule: = expected"))
     end
 
-fun read_term f g s = 
+fun read_term f g s =
     let
-	val t = tokenize s
-	val (ts, term) = parse_term f g t
+        val t = tokenize s
+        val (ts, term) = parse_term f g t
     in
-	case ts of 
-	    [] => term
-	  | _ => raise (Parse ("read_term: still tokens left, end expected"))
+        case ts of
+            [] => term
+          | _ => raise (Parse ("read_term: still tokens left, end expected"))
     end
 
 end
diff -r 228d663cc9b3 -r 5979c46853d1 src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Jul 14 19:28:23 2005 +0200
+++ b/src/Pure/library.ML	Thu Jul 14 19:28:24 2005 +0200
@@ -8,19 +8,20 @@
 tables, balanced trees, orders, current directory, misc.
 *)
 
-infix |> |-> ||> ||>> |>> |>>> #> #-> ~~ \ \\ ins ins_string ins_int orf andf prefix upto downto
-  mem mem_int mem_string union union_int union_string inter inter_int
-  inter_string subset subset_int subset_string;
+infix |> |-> ||> ||>> |>> |>>> #> #-> ~~ \ \\ ins ins_string ins_int
+  orf andf prefix upto downto mem mem_int mem_string union union_int
+  union_string inter inter_int inter_string subset subset_int
+  subset_string;
 
 infix 3 oo ooo oooo;
 
 signature BASIC_LIBRARY =
 sig
   (*functions*)
+  val I: 'a -> 'a
+  val K: 'a -> 'b -> 'a
   val curry: ('a * 'b -> 'c) -> 'a -> 'b -> 'c
   val uncurry: ('a -> 'b -> 'c) -> 'a * 'b -> 'c
-  val I: 'a -> 'a
-  val K: 'a -> 'b -> 'a
   val |> : 'a * ('a -> 'b) -> 'b
   val |-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b
   val ||> : ('c * 'a) * ('a -> 'b) -> 'c * 'b
@@ -33,9 +34,9 @@
   val oo: ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b
   val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b
   val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b
+  val funpow: int -> ('a -> 'a) -> 'a -> 'a
   val apl: 'a * ('a * 'b -> 'c) -> 'b -> 'c
   val apr: ('a * 'b -> 'c) * 'b -> 'a -> 'c
-  val funpow: int -> ('a -> 'a) -> 'a -> 'a
 
   (*old options -- invalidated*)
   datatype invalid = None of invalid
@@ -295,11 +296,10 @@
 
 (** functions **)
 
-(*handy combinators*)
+fun I x = x;
+fun K x = fn _ => x;
 fun curry f x y = f (x, y);
 fun uncurry f (x, y) = f x y;
-fun I x = x;
-fun K x = fn _ => x;
 
 (*reverse application and structured results*)
 fun x |> f = f x;
@@ -308,25 +308,28 @@
 fun (x, y) ||> f = (x, f y);
 fun (x, y) |>>> f = let val (x', z) = f x in (x', (y, z)) end;
 fun (x, y) ||>> f = let val (z, y') = f y in ((x, z), y') end;
+
+(*reverse composition*)
 fun f #> g = g o f;
-fun f #-> g = fn s => let val (v, s') = f s in g v s' end;
-fun ` h = fn s => (h s, s)
+fun f #-> g = uncurry g o f;
+
+(*view results*)
+fun `f = fn x => (f x, x);
 
 (*composition with multiple args*)
 fun (f oo g) x y = f (g x y);
 fun (f ooo g) x y z = f (g x y z);
 fun (f oooo g) x y z w = f (g x y z w);
 
-(*application of (infix) operator to its left or right argument*)
-fun apl (x, f) y = f (x, y);
-fun apr (f, y) x = f (x, y);
-
 (*function exponentiation: f(...(f x)...) with n applications of f*)
 fun funpow n f x =
   let fun rep (0, x) = x
         | rep (n, x) = rep (n - 1, f x)
   in rep (n, x) end;
 
+(*application of (infix) operator to its left or right argument*)
+fun apl (x, f) y = f (x, y);
+fun apr (f, y) x = f (x, y);
 
 
 (** options **)
@@ -1268,12 +1271,13 @@
   Preserves order of elements in both lists.*)
 val partition = List.partition;
 
-
 fun partition_eq (eq:'a * 'a -> bool) =
-    let fun part [] = []
-          | part (x::ys) = let val (xs, xs') = partition (apl(x, eq)) ys
-                           in (x::xs)::(part xs') end
-    in part end;
+  let
+    fun part [] = []
+      | part (x :: ys) =
+          let val (xs, xs') = partition (fn y => eq (x, y)) ys
+          in (x::xs)::(part xs') end
+  in part end;
 
 
 (*Partition a list into buckets  [ bi, b(i+1), ..., bj ]
diff -r 228d663cc9b3 -r 5979c46853d1 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Thu Jul 14 19:28:23 2005 +0200
+++ b/src/Pure/meta_simplifier.ML	Thu Jul 14 19:28:24 2005 +0200
@@ -419,7 +419,7 @@
   andalso not(exists_subterm is_Var lhs)
     orelse
 *)
-  exists (apl (lhs, Logic.occs)) (rhs :: prems)
+  exists (fn t => Logic.occs (lhs, t)) (rhs :: prems)
     orelse
   null prems andalso Pattern.matches (Sign.tsig_of thy) (lhs, rhs)
     (*the condition "null prems" is necessary because conditional rewrites
diff -r 228d663cc9b3 -r 5979c46853d1 src/Pure/net.ML
--- a/src/Pure/net.ML	Thu Jul 14 19:28:23 2005 +0200
+++ b/src/Pure/net.ML	Thu Jul 14 19:28:24 2005 +0200
@@ -222,10 +222,10 @@
       | subtr (Leaf _) (net as Net _) = subtr emptynet net
       | subtr (Net {comb = comb1, var = var1, atoms = atoms1})
             (Net {comb = comb2, var = var2, atoms = atoms2}) =
-          Symtab.fold (fn (a, net) =>
-            subtr (if_none (Symtab.lookup (atoms1, a)) emptynet) net) atoms2 o
-          subtr var1 var2 o
-          subtr comb1 comb2;
+          subtr comb1 comb2
+          #> subtr var1 var2
+          #> Symtab.fold (fn (a, net) =>
+            subtr (if_none (Symtab.lookup (atoms1, a)) emptynet) net) atoms2
   in subtr net1 net2 [] end;
 
 fun entries net = subtract (K false) empty net;