# HG changeset patch
# User wenzelm
# Date 1208012445 -7200
# Node ID d6b6c74a8bcf229f5cdb77c750c74cef7c0d374f
# Parent  3074b3de4f4f649a537073bbd8a7ca9d61ed3901
rep_cterm/rep_thm: no longer dereference theory_ref;
removed obsolete compression;

diff -r 3074b3de4f4f -r d6b6c74a8bcf src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Apr 12 17:00:43 2008 +0200
+++ b/src/Pure/proofterm.ML	Sat Apr 12 17:00:45 2008 +0200
@@ -916,16 +916,13 @@
 
 fun shrink_proof thy =
   let
-    val compress_typ = Compress.typ thy;
-    val compress_term = Compress.term thy;
-
     fun shrink ls lev (prf as Abst (a, T, body)) =
           let val (b, is, ch, body') = shrink ls (lev+1) body
-          in (b, is, ch, if ch then Abst (a, Option.map compress_typ T, body') else prf) end
+          in (b, is, ch, if ch then Abst (a, T, body') else prf) end
       | shrink ls lev (prf as AbsP (a, t, body)) =
           let val (b, is, ch, body') = shrink (lev::ls) lev body
           in (b orelse member (op =) is 0, map_filter (fn 0 => NONE | i => SOME (i-1)) is,
-            ch, if ch then AbsP (a, Option.map compress_term t, body') else prf)
+            ch, if ch then AbsP (a, t, body') else prf)
           end
       | shrink ls lev prf =
           let val (is, ch, _, prf') = shrink' ls lev [] [] prf
@@ -940,13 +937,13 @@
       | shrink' ls lev ts prfs (prf as prf1 % t) =
           let val (is, ch, (ch', t')::ts', prf') = shrink' ls lev (t::ts) prfs prf1
           in (is, ch orelse ch', ts',
-              if ch orelse ch' then prf' % Option.map compress_term t' else prf) end
+              if ch orelse ch' then prf' % t' else prf) end
       | shrink' ls lev ts prfs (prf as PBound i) =
           (if exists (fn SOME (Bound j) => lev-j <= List.nth (ls, i) | _ => true) ts
              orelse has_duplicates (op =)
                (Library.foldl (fn (js, SOME (Bound j)) => j :: js | (js, _) => js) ([], ts))
              orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf)
-      | shrink' ls lev ts prfs (Hyp t) = ([], false, map (pair false) ts, Hyp (compress_term t))
+      | shrink' ls lev ts prfs (Hyp t) = ([], false, map (pair false) ts, Hyp t)
       | shrink' ls lev ts prfs (prf as MinProof _) =
           ([], false, map (pair false) ts, prf)
       | shrink' ls lev ts prfs prf =
diff -r 3074b3de4f4f -r d6b6c74a8bcf src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sat Apr 12 17:00:43 2008 +0200
+++ b/src/Pure/sign.ML	Sat Apr 12 17:00:45 2008 +0200
@@ -661,7 +661,7 @@
         val c' = if authentic then Syntax.constN ^ full_c else c;
         val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
           cat_error msg ("in declaration of constant " ^ quote c);
-        val T' = Compress.typ thy (Logic.varifyT T);
+        val T' = Logic.varifyT T;
       in ((c, T'), (c', T', mx), Const (full_c, T)) end;
     val args = map prep raw_args;
   in
@@ -686,7 +686,7 @@
 fun add_abbrev mode tags (c, raw_t) thy =
   let
     val pp = pp thy;
-    val prep_tm = Compress.term thy o no_frees pp o Term.no_dummy_patterns o cert_term_abbrev thy;
+    val prep_tm = no_frees pp o Term.no_dummy_patterns o cert_term_abbrev thy;
     val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
       handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
     val (res, consts') = consts_of thy
diff -r 3074b3de4f4f -r d6b6c74a8bcf src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sat Apr 12 17:00:43 2008 +0200
+++ b/src/Pure/theory.ML	Sat Apr 12 17:00:45 2008 +0200
@@ -211,7 +211,7 @@
 
 fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
   let
-    val axms = map (apsnd (Compress.term thy o Logic.varify) o prep_axm thy) raw_axms;
+    val axms = map (apsnd Logic.varify o prep_axm thy) raw_axms;
     val axioms' = NameSpace.extend_table (Sign.naming_of thy) axms axioms
       handle Symtab.DUP dup => err_dup_axm dup;
   in axioms' end);
@@ -235,7 +235,7 @@
     val consts = Sign.consts_of thy;
     fun prep const =
       let val Const (c, T) = Sign.no_vars pp (Const const)
-      in (c, Consts.typargs consts (c, Compress.typ thy (Logic.varifyT T))) end;
+      in (c, Consts.typargs consts (c, Logic.varifyT T)) end;
 
     val lhs_vars = Term.add_tfreesT (#2 lhs) [];
     val rhs_extras = fold (#2 #> Term.fold_atyps (fn TFree v =>
diff -r 3074b3de4f4f -r d6b6c74a8bcf src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Apr 12 17:00:43 2008 +0200
+++ b/src/Pure/thm.ML	Sat Apr 12 17:00:45 2008 +0200
@@ -12,7 +12,7 @@
   (*certified types*)
   type ctyp
   val rep_ctyp: ctyp ->
-   {thy: theory,
+   {thy_ref: theory_ref,
     T: typ,
     maxidx: int,
     sorts: sort list}
@@ -24,12 +24,12 @@
   type cterm
   exception CTERM of string * cterm list
   val rep_cterm: cterm ->
-   {thy: theory,
+   {thy_ref: theory_ref,
     t: term,
     T: typ,
     maxidx: int,
     sorts: sort list}
-  val crep_cterm: cterm -> {thy: theory, t: term, T: ctyp, maxidx: int, sorts: sort list}
+  val crep_cterm: cterm -> {thy_ref: theory_ref, t: term, T: ctyp, maxidx: int, sorts: sort list}
   val theory_of_cterm: cterm -> theory
   val term_of: cterm -> term
   val cterm_of: theory -> term -> cterm
@@ -40,7 +40,7 @@
   type conv = cterm -> thm
   type attribute = Context.generic * thm -> Context.generic * thm
   val rep_thm: thm ->
-   {thy: theory,
+   {thy_ref: theory_ref,
     der: bool * Proofterm.proof,
     tags: Markup.property list,
     maxidx: int,
@@ -49,7 +49,7 @@
     tpairs: (term * term) list,
     prop: term}
   val crep_thm: thm ->
-   {thy: theory,
+   {thy_ref: theory_ref,
     der: bool * Proofterm.proof,
     tags: Markup.property list,
     maxidx: int,
@@ -140,7 +140,6 @@
   val put_name: string -> thm -> thm
   val get_tags: thm -> Markup.property list
   val map_tags: (Markup.property list -> Markup.property list) -> thm -> thm
-  val compress: thm -> thm
   val norm_proof: thm -> thm
   val adjust_maxidx_thm: int -> thm -> thm
   val rename_boundvars: term -> term -> thm -> thm
@@ -181,12 +180,8 @@
   sorts: sort list}
 with
 
-fun rep_ctyp (Ctyp {thy_ref, T, maxidx, sorts}) =
-  let val thy = Theory.deref thy_ref
-  in {thy = thy, T = T, maxidx = maxidx, sorts = sorts} end;
-
+fun rep_ctyp (Ctyp args) = args;
 fun theory_of_ctyp (Ctyp {thy_ref, ...}) = Theory.deref thy_ref;
-
 fun typ_of (Ctyp {T, ...}) = T;
 
 fun ctyp_of thy raw_T =
@@ -215,16 +210,11 @@
 
 exception CTERM of string * cterm list;
 
-fun rep_cterm (Cterm {thy_ref, t, T, maxidx, sorts}) =
-  let val thy =  Theory.deref thy_ref
-  in {thy = thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end;
+fun rep_cterm (Cterm args) = args;
 
 fun crep_cterm (Cterm {thy_ref, t, T, maxidx, sorts}) =
-  let val thy = Theory.deref thy_ref in
-   {thy = thy, t = t,
-      T = Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts},
-    maxidx = maxidx, sorts = sorts}
-  end;
+  {thy_ref = thy_ref, t = t, maxidx = maxidx, sorts = sorts,
+    T = Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts}};
 
 fun theory_of_cterm (Cterm {thy_ref, ...}) = Theory.deref thy_ref;
 fun term_of (Cterm {t, ...}) = t;
@@ -376,19 +366,11 @@
 (*errors involving theorems*)
 exception THM of string * int * thm list;
 
-fun rep_thm (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
-  let val thy = Theory.deref thy_ref in
-   {thy = thy, der = der, tags = tags, maxidx = maxidx,
-    shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}
-  end;
+fun rep_thm (Thm args) = args;
 
-(*version of rep_thm returning cterms instead of terms*)
 fun crep_thm (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
-  let
-    val thy = Theory.deref thy_ref;
-    fun cterm max t = Cterm {thy_ref = thy_ref, t = t, T = propT, maxidx = max, sorts = shyps};
-  in
-   {thy = thy, der = der, tags = tags, maxidx = maxidx, shyps = shyps,
+  let fun cterm max t = Cterm {thy_ref = thy_ref, t = t, T = propT, maxidx = max, sorts = shyps} in
+   {thy_ref = thy_ref, der = der, tags = tags, maxidx = maxidx, shyps = shyps,
     hyps = map (cterm ~1) hyps,
     tpairs = map (pairself (cterm maxidx)) tpairs,
     prop = cterm maxidx prop}
@@ -578,25 +560,6 @@
     shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop};
 
 
-(*Compression of theorems -- a separate rule, not integrated with the others,
-  as it could be slow.*)
-fun compress (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
-  let
-    val thy = Theory.deref thy_ref;
-    val hyps' = map (Compress.term thy) hyps;
-    val tpairs' = map (pairself (Compress.term thy)) tpairs;
-    val prop' = Compress.term thy prop;
-  in
-    Thm {thy_ref = Theory.check_thy thy,
-      der = der,
-      tags = tags,
-      maxidx = maxidx,
-      shyps = shyps,
-      hyps = hyps',
-      tpairs = tpairs',
-      prop = prop'}
-  end;
-
 fun norm_proof (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
   let
     val thy = Theory.deref thy_ref;