Compress.term;

--- a/src/Pure/theory.ML	Mon Aug 01 19:20:44 2005 +0200
+++ b/src/Pure/theory.ML	Mon Aug 01 19:20:45 2005 +0200
@@ -207,7 +207,7 @@
 
 fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
   let
-    val axms = map (apsnd (Term.compress_term o Logic.varify) o prep_axm thy) raw_axms;
+    val axms = map (apsnd (Compress.term thy o Logic.varify) o prep_axm thy) raw_axms;
     val axioms' = NameSpace.extend_table (Sign.naming_of thy) (axioms, axms)
       handle Symtab.DUPS dups => err_dup_axms dups;
   in axioms' end);
@@ -303,9 +303,9 @@
     val _ = check_overloading thy overloaded const;
   in
     defs
-    |> Defs.declare (declared const)
-    |> fold (Defs.declare o declared) rhs_consts
-    |> Defs.define pp const (Sign.full_name thy bname) rhs_consts
+    |> Defs.declare thy (declared const)
+    |> fold (Defs.declare thy o declared) rhs_consts
+    |> Defs.define thy const (Sign.full_name thy bname) rhs_consts
   end
   handle ERROR => error (Pretty.string_of (Pretty.block
    [Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"),
@@ -338,7 +338,7 @@
 fun gen_add_finals prep_term overloaded raw_terms thy =
   let
     val pp = Sign.pp thy;
-    fun finalize tm finals =
+    fun finalize tm =
       let
         val _ = no_vars pp tm;
         val const as (c, _) =
@@ -346,8 +346,8 @@
           | Free _ => error "Attempt to finalize variable (or undeclared constant)"
           | _ => error "Attempt to finalize non-constant term")
           |> check_overloading thy overloaded;
-      in finals |> Defs.declare (c, Sign.the_const_type thy c) |> Defs.finalize const end;
-  in thy |> map_defs (fold finalize (map (prep_term thy) raw_terms)) end;
+      in Defs.declare thy (c, Sign.the_const_type thy c) #> Defs.finalize thy const end;
+  in thy |> map_defs (fold (finalize o prep_term thy) raw_terms) end;
 
 fun read_term thy = Sign.simple_read_term thy TypeInfer.logicT;
 fun cert_term thy = #1 o Sign.certify_term (Sign.pp thy) thy;

--- a/src/Pure/thm.ML	Mon Aug 01 19:20:44 2005 +0200
+++ b/src/Pure/thm.ML	Mon Aug 01 19:20:45 2005 +0200
@@ -573,13 +573,15 @@
 (*Compression of theorems -- a separate rule, not integrated with the others,
   as it could be slow.*)
 fun compress (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
-  Thm {thy_ref = thy_ref,
-    der = der,
-    maxidx = maxidx,
-    shyps = shyps,
-    hyps = map Term.compress_term hyps,
-    tpairs = map (pairself Term.compress_term) tpairs,
-    prop = Term.compress_term prop};
+  let val thy = Theory.deref thy_ref in
+    Thm {thy_ref = thy_ref,
+      der = der,
+      maxidx = maxidx,
+      shyps = shyps,
+      hyps = map (Compress.term thy) hyps,
+      tpairs = map (pairself (Compress.term thy)) tpairs,
+      prop = Compress.term thy prop}
+  end;
 
 fun adjust_maxidx_thm (Thm {thy_ref, der, shyps, hyps, tpairs, prop, ...}) =
   Thm {thy_ref = thy_ref,
@@ -1310,7 +1312,7 @@
         (*unknowns appearing elsewhere be preserved!*)
         val vids = map (#1 o #1 o dest_Var) vars;
         fun rename(t as Var((x,i),T)) =
-                (case assoc(al,x) of
+                (case assoc_string (al,x) of
                    SOME(y) => if x mem_string vids orelse y mem_string vids then t
                               else Var((y,i),T)
                  | NONE=> t)