--- a/src/Pure/Concurrent/task_queue.ML Thu Jul 14 22:08:11 2011 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Thu Jul 14 22:53:43 2011 +0200
@@ -318,7 +318,7 @@
| ready (task :: tasks) rest =
(case try (Task_Graph.get_entry jobs) task of
NONE => ready tasks rest
- | SOME entry =>
+ | SOME (_, entry) =>
(case ready_job task entry of
NONE => ready tasks (task :: rest)
| some => (some, List.revAppend (rest, tasks))));
@@ -327,7 +327,7 @@
| ready_dep seen (task :: tasks) =
if Tasks.defined seen task then ready_dep seen tasks
else
- let val entry as (_, (ds, _)) = Task_Graph.get_entry jobs task in
+ let val entry as (_, (ds, _)) = #2 (Task_Graph.get_entry jobs task) in
(case ready_job task entry of
NONE => ready_dep (Tasks.update (task, ()) seen) (ds @ tasks)
| some => some)
--- a/src/Pure/General/graph.ML Thu Jul 14 22:08:11 2011 +0200
+++ b/src/Pure/General/graph.ML Thu Jul 14 22:53:43 2011 +0200
@@ -20,7 +20,7 @@
val minimals: 'a T -> key list
val maximals: 'a T -> key list
val subgraph: (key -> bool) -> 'a T -> 'a T
- val get_entry: 'a T -> key -> 'a * (key list * key list) (*exception UNDEF*)
+ val get_entry: 'a T -> key -> key * ('a * (key list * key list)) (*exception UNDEF*)
val map: (key -> 'a -> 'b) -> 'a T -> 'b T
val get_node: 'a T -> key -> 'a (*exception UNDEF*)
val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
@@ -101,14 +101,14 @@
in Graph (fold_graph subg G Table.empty) end;
fun get_entry (Graph tab) x =
- (case Table.lookup tab x of
+ (case Table.lookup_key tab x of
SOME entry => entry
| NONE => raise UNDEF x);
-fun map_entry x f (G as Graph tab) = Graph (Table.update (x, f (get_entry G x)) tab);
+fun map_entry x f (G as Graph tab) = Graph (Table.update (x, f (#2 (get_entry G x))) tab);
fun map_entry_yield x f (G as Graph tab) =
- let val (a, node') = f (get_entry G x)
+ let val (a, node') = f (#2 (get_entry G x))
in (a, Graph (Table.update (x, node') tab)) end;
@@ -116,7 +116,7 @@
fun map_nodes f (Graph tab) = Graph (Table.map (apfst o f) tab);
-fun get_node G = #1 o get_entry G;
+fun get_node G = #1 o #2 o get_entry G;
fun map_node x f = map_entry x (fn (i, ps) => (f i, ps));
@@ -137,8 +137,8 @@
in fold reachs xs ([], empty_keys) end;
(*immediate*)
-fun imm_preds G = #1 o #2 o get_entry G;
-fun imm_succs G = #2 o #2 o get_entry G;
+fun imm_preds G = #1 o #2 o #2 o get_entry G;
+fun imm_succs G = #2 o #2 o #2 o get_entry G;
(*transitive*)
fun all_preds G = flat o #1 o reachable (imm_preds G);
@@ -167,7 +167,7 @@
fun del_node x (G as Graph tab) =
let
fun del_adjacent which y = Table.map_entry y (fn (i, ps) => (i, (which (remove_key x) ps)));
- val (preds, succs) = #2 (get_entry G x);
+ val (preds, succs) = #2 (#2 (get_entry G x));
in
Graph (tab
|> Table.delete x
--- a/src/Pure/General/markup.ML Thu Jul 14 22:08:11 2011 +0200
+++ b/src/Pure/General/markup.ML Thu Jul 14 22:53:43 2011 +0200
@@ -136,9 +136,11 @@
(* integers *)
fun parse_int s =
- (case Int.fromString s of
- SOME i => i
- | NONE => raise Fail ("Bad integer: " ^ quote s));
+ let val i = Int.fromString s in
+ if is_none i orelse String.isPrefix "~" s
+ then raise Fail ("Bad integer: " ^ quote s)
+ else the i
+ end;
val print_int = signed_string_of_int;
--- a/src/Pure/General/table.ML Thu Jul 14 22:08:11 2011 +0200
+++ b/src/Pure/General/table.ML Thu Jul 14 22:53:43 2011 +0200
@@ -30,6 +30,7 @@
val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option
val exists: (key * 'a -> bool) -> 'a table -> bool
val forall: (key * 'a -> bool) -> 'a table -> bool
+ val lookup_key: 'a table -> key -> (key * 'a) option
val lookup: 'a table -> key -> 'a option
val defined: 'a table -> key -> bool
val update: key * 'a -> 'a table -> 'a table
@@ -161,25 +162,27 @@
(* lookup *)
-fun lookup tab key =
+fun lookup_key tab key =
let
fun look Empty = NONE
| look (Branch2 (left, (k, x), right)) =
(case Key.ord (key, k) of
LESS => look left
- | EQUAL => SOME x
+ | EQUAL => SOME (k, x)
| GREATER => look right)
| look (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
(case Key.ord (key, k1) of
LESS => look left
- | EQUAL => SOME x1
+ | EQUAL => SOME (k1, x1)
| GREATER =>
(case Key.ord (key, k2) of
LESS => look mid
- | EQUAL => SOME x2
+ | EQUAL => SOME (k2, x2)
| GREATER => look right));
in look tab end;
+fun lookup tab key = Option.map #2 (lookup_key tab key);
+
fun defined tab key =
let
fun def Empty = false
--- a/src/Pure/General/xml.ML Thu Jul 14 22:08:11 2011 +0200
+++ b/src/Pure/General/xml.ML Thu Jul 14 22:53:43 2011 +0200
@@ -38,6 +38,7 @@
val element: string -> attributes -> string list -> string
val output_markup: Markup.T -> Output.output * Output.output
val string_of: tree -> string
+ val pretty: int -> tree -> Pretty.T
val output: tree -> TextIO.outstream -> unit
val parse_comments: string list -> unit * string list
val parse_string : string -> string option
@@ -112,19 +113,24 @@
(* output *)
-fun buffer_of tree =
+fun buffer_of depth tree =
let
- fun traverse (Elem ((name, atts), [])) =
+ fun traverse _ (Elem ((name, atts), [])) =
Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add "/>"
- | traverse (Elem ((name, atts), ts)) =
+ | traverse d (Elem ((name, atts), ts)) =
Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add ">" #>
- fold traverse ts #>
+ traverse_body d ts #>
Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
- | traverse (Text s) = Buffer.add (text s);
- in Buffer.empty |> traverse tree end;
+ | traverse _ (Text s) = Buffer.add (text s)
+ and traverse_body 0 _ = Buffer.add "..."
+ | traverse_body d ts = fold (traverse (d - 1)) ts;
+ in Buffer.empty |> traverse depth tree end;
-val string_of = Buffer.content o buffer_of;
-val output = Buffer.output o buffer_of;
+val string_of = Buffer.content o buffer_of ~1;
+val output = Buffer.output o buffer_of ~1;
+
+fun pretty depth tree =
+ Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree));
@@ -287,9 +293,8 @@
(* atomic values *)
fun int_atom s =
- (case Int.fromString s of
- SOME i => i
- | NONE => raise XML_ATOM s);
+ Markup.parse_int s
+ handle Fail _ => raise XML_ATOM s;
fun bool_atom "0" = false
| bool_atom "1" = true
--- a/src/Pure/IsaMakefile Thu Jul 14 22:08:11 2011 +0200
+++ b/src/Pure/IsaMakefile Thu Jul 14 22:53:43 2011 +0200
@@ -248,6 +248,7 @@
tactical.ML \
term.ML \
term_ord.ML \
+ term_sharing.ML \
term_subst.ML \
term_xml.ML \
theory.ML \
--- a/src/Pure/Isar/generic_target.ML Thu Jul 14 22:08:11 2011 +0200
+++ b/src/Pure/Isar/generic_target.ML Thu Jul 14 22:53:43 2011 +0200
@@ -118,7 +118,7 @@
|> Drule.zero_var_indexes_list;
(*thm definition*)
- val result = Global_Theory.name_thm true true name th'';
+ val result = Global_Theory.name_thm true true name (Thm.compress th'');
(*import fixes*)
val (tvars, vars) =
--- a/src/Pure/Isar/proof_context.ML Thu Jul 14 22:08:11 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML Thu Jul 14 22:53:43 2011 +0200
@@ -449,7 +449,7 @@
Const (d, Consts.type_scheme (consts_of ctxt) d handle TYPE (msg, _, _) => err msg)
| NONE => Consts.read_const consts (c, pos));
val _ =
- if strict then ignore (Consts.the_type consts d) handle TYPE (msg, _, _) => err msg
+ if strict then ignore (Consts.the_const consts d) handle TYPE (msg, _, _) => err msg
else ();
val _ = Context_Position.report ctxt pos (Name_Space.markup (Consts.space_of consts) d);
in t end;
--- a/src/Pure/ML/install_pp_polyml-5.3.ML Thu Jul 14 22:08:11 2011 +0200
+++ b/src/Pure/ML/install_pp_polyml-5.3.ML Thu Jul 14 22:53:43 2011 +0200
@@ -7,6 +7,9 @@
PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str)));
+PolyML.addPrettyPrinter (fn depth => fn _ => fn tree =>
+ ml_pretty (Pretty.to_ML (XML.pretty depth tree)));
+
PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
pretty (Synchronized.value var, depth));
--- a/src/Pure/ML/ml_antiquote.ML Thu Jul 14 22:08:11 2011 +0200
+++ b/src/Pure/ML/ml_antiquote.ML Thu Jul 14 22:53:43 2011 +0200
@@ -161,7 +161,7 @@
val _ = Context.>> (Context.map_theory
(inline (Binding.name "const_name")
- (const_name (fn (consts, c) => (Consts.the_type consts c; c))) #>
+ (const_name (fn (consts, c) => (Consts.the_const consts c; c))) #>
inline (Binding.name "const_abbrev")
(const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #>
inline (Binding.name "const_syntax")
--- a/src/Pure/ROOT.ML Thu Jul 14 22:08:11 2011 +0200
+++ b/src/Pure/ROOT.ML Thu Jul 14 22:53:43 2011 +0200
@@ -52,8 +52,8 @@
use "General/graph.ML";
use "General/linear_set.ML";
use "General/buffer.ML";
+use "General/pretty.ML";
use "General/xml.ML";
-use "General/pretty.ML";
use "General/path.ML";
use "General/url.ML";
use "General/file.ML";
@@ -140,6 +140,7 @@
use "primitive_defs.ML";
use "defs.ML";
use "sign.ML";
+use "term_sharing.ML";
use "pattern.ML";
use "unify.ML";
use "theory.ML";
--- a/src/Pure/Syntax/syntax_phases.ML Thu Jul 14 22:08:11 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Thu Jul 14 22:53:43 2011 +0200
@@ -709,8 +709,8 @@
(** check/uncheck **)
-val check_typs = Syntax.typ_check;
-val check_terms = Syntax.term_check;
+fun check_typs ctxt = Syntax.typ_check ctxt #> Term_Sharing.typs (Proof_Context.theory_of ctxt);
+fun check_terms ctxt = Syntax.term_check ctxt #> Term_Sharing.terms (Proof_Context.theory_of ctxt);
fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
val uncheck_typs = Syntax.typ_uncheck;
--- a/src/Pure/consts.ML Thu Jul 14 22:08:11 2011 +0200
+++ b/src/Pure/consts.ML Thu Jul 14 22:53:43 2011 +0200
@@ -13,7 +13,7 @@
val dest: T ->
{constants: (typ * term option) Name_Space.table,
constraints: typ Name_Space.table}
- val the_type: T -> string -> typ (*exception TYPE*)
+ val the_const: T -> string -> string * typ (*exception TYPE*)
val the_abbreviation: T -> string -> typ * term (*exception TYPE*)
val type_scheme: T -> string -> typ (*exception TYPE*)
val is_monomorphic: T -> string -> bool (*exception TYPE*)
@@ -92,22 +92,22 @@
(* lookup consts *)
-fun the_const (Consts {decls = (_, tab), ...}) c =
- (case Symtab.lookup tab c of
- SOME decl => decl
+fun the_entry (Consts {decls = (_, tab), ...}) c =
+ (case Symtab.lookup_key tab c of
+ SOME entry => entry
| NONE => raise TYPE ("Unknown constant: " ^ quote c, [], []));
-fun the_type consts c =
- (case the_const consts c of
- ({T, ...}, NONE) => T
+fun the_const consts c =
+ (case the_entry consts c of
+ (c', ({T, ...}, NONE)) => (c', T)
| _ => raise TYPE ("Not a logical constant: " ^ quote c, [], []));
fun the_abbreviation consts c =
- (case the_const consts c of
- ({T, ...}, SOME {rhs, ...}) => (T, rhs)
+ (case the_entry consts c of
+ (_, ({T, ...}, SOME {rhs, ...})) => (T, rhs)
| _ => raise TYPE ("Not an abbreviated constant: " ^ quote c, [], []));
-val the_decl = #1 oo the_const;
+fun the_decl consts = #1 o #2 o the_entry consts;
val type_scheme = #T oo the_decl;
val type_arguments = #typargs oo the_decl;
@@ -170,7 +170,7 @@
| Const (c, T) =>
let
val T' = certT T;
- val ({T = U, ...}, abbr) = the_const consts c;
+ val (_, ({T = U, ...}, abbr)) = the_entry consts c;
fun expand u =
Term.betapplys (Envir.expand_atom T' (U, u) handle TYPE _ =>
err "Illegal type for abbreviation" (c, T), args');
@@ -245,7 +245,7 @@
fun constrain (c, C) consts =
consts |> map_consts (fn (decls, constraints, rev_abbrevs) =>
- (the_const consts c handle TYPE (msg, _, _) => error msg;
+ (#2 (the_entry consts c) handle TYPE (msg, _, _) => error msg;
(decls,
constraints |> (case C of SOME T => Symtab.update (c, T) | NONE => Symtab.delete_safe c),
rev_abbrevs)));
--- a/src/Pure/library.ML Thu Jul 14 22:08:11 2011 +0200
+++ b/src/Pure/library.ML Thu Jul 14 22:53:43 2011 +0200
@@ -908,7 +908,8 @@
val string_ord = String.compare;
fun fast_string_ord (s1, s2) =
- (case int_ord (size s1, size s2) of EQUAL => string_ord (s1, s2) | ord => ord);
+ if pointer_eq (s1, s2) then EQUAL
+ else (case int_ord (size s1, size s2) of EQUAL => string_ord (s1, s2) | ord => ord);
fun option_ord ord (SOME x, SOME y) = ord (x, y)
| option_ord _ (NONE, NONE) = EQUAL
--- a/src/Pure/proofterm.ML Thu Jul 14 22:08:11 2011 +0200
+++ b/src/Pure/proofterm.ML Thu Jul 14 22:53:43 2011 +0200
@@ -1048,15 +1048,17 @@
if ! proofs = 0 then ((name, dummy), Oracle (name, dummy, NONE))
else ((name, prop), gen_axm_proof Oracle name prop);
-val shrink_proof =
+fun shrink_proof thy =
let
+ val (typ, term) = Term_Sharing.init 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, T, body') else prf) end
+ in (b, is, ch, if ch then Abst (a, Option.map typ 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, t, body') else prf)
+ ch, if ch then AbsP (a, Option.map term t, body') else prf)
end
| shrink ls lev prf =
let val (is, ch, _, prf') = shrink' ls lev [] [] prf
@@ -1071,13 +1073,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' % t' else prf) end
+ if ch orelse ch' then prf' % Option.map term t' else prf) end
| shrink' ls lev ts prfs (prf as PBound i) =
(if exists (fn SOME (Bound j) => lev-j <= 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 (prf as Hyp _) = ([], false, map (pair false) ts, prf)
+ | shrink' ls lev ts prfs (Hyp t) = ([], false, map (pair false) ts, Hyp (term t))
| shrink' ls lev ts prfs (prf as MinProof) = ([], false, map (pair false) ts, prf)
| shrink' ls lev ts prfs (prf as OfClass _) = ([], false, map (pair false) ts, prf)
| shrink' ls lev ts prfs prf =
@@ -1442,7 +1444,7 @@
val argsP = map OfClass outer_constraints @ map Hyp hyps;
fun full_proof0 () =
- #4 (shrink_proof [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)));
+ #4 (shrink_proof thy [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)));
fun make_body0 proof0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
val body0 =
--- a/src/Pure/pure_setup.ML Thu Jul 14 22:08:11 2011 +0200
+++ b/src/Pure/pure_setup.ML Thu Jul 14 22:53:43 2011 +0200
@@ -18,7 +18,6 @@
(* ML toplevel pretty printing *)
-toplevel_pp ["XML", "tree"] "Pretty.str o XML.string_of";
toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
--- a/src/Pure/sign.ML Thu Jul 14 22:08:11 2011 +0200
+++ b/src/Pure/sign.ML Thu Jul 14 22:53:43 2011 +0200
@@ -210,7 +210,7 @@
val consts_of = #consts o rep_sg;
val the_const_constraint = Consts.the_constraint o consts_of;
-val the_const_type = Consts.the_type o consts_of;
+val the_const_type = #2 oo (Consts.the_const o consts_of);
val const_type = try o the_const_type;
val const_monomorphic = Consts.is_monomorphic o consts_of;
val const_typargs = Consts.typargs o consts_of;
--- a/src/Pure/sorts.ML Thu Jul 14 22:08:11 2011 +0200
+++ b/src/Pure/sorts.ML Thu Jul 14 22:53:43 2011 +0200
@@ -185,8 +185,8 @@
(* certify *)
fun certify_class algebra c =
- if can (Graph.get_node (classes_of algebra)) c then c
- else raise TYPE ("Undeclared class: " ^ quote c, [], []);
+ #1 (Graph.get_entry (classes_of algebra) c)
+ handle Graph.UNDEF _ => raise TYPE ("Undeclared class: " ^ quote c, [], []);
fun certify_sort classes = map (certify_class classes);
--- a/src/Pure/term_ord.ML Thu Jul 14 22:08:11 2011 +0200
+++ b/src/Pure/term_ord.ML Thu Jul 14 22:53:43 2011 +0200
@@ -19,6 +19,7 @@
val sort_ord: sort * sort -> order
val typ_ord: typ * typ -> order
val fast_term_ord: term * term -> order
+ val syntax_term_ord: term * term -> order
val indexname_ord: indexname * indexname -> order
val tvar_ord: (indexname * sort) * (indexname * sort) -> order
val var_ord: (indexname * typ) * (indexname * typ) -> order
@@ -84,7 +85,7 @@
| atoms_ord (Free (x, _), Free (y, _)) = fast_string_ord (x, y)
| atoms_ord (Var (xi, _), Var (yj, _)) = fast_indexname_ord (xi, yj)
| atoms_ord (Bound i, Bound j) = int_ord (i, j)
- | atoms_ord _ = raise Fail "atoms_ord";
+ | atoms_ord _ = EQUAL;
fun types_ord (Abs (_, T, t), Abs (_, U, u)) =
(case typ_ord (T, U) of EQUAL => types_ord (t, u) | ord => ord)
@@ -93,8 +94,13 @@
| types_ord (Const (_, T), Const (_, U)) = typ_ord (T, U)
| types_ord (Free (_, T), Free (_, U)) = typ_ord (T, U)
| types_ord (Var (_, T), Var (_, U)) = typ_ord (T, U)
- | types_ord (Bound _, Bound _) = EQUAL
- | types_ord _ = raise Fail "types_ord";
+ | types_ord _ = EQUAL;
+
+fun comments_ord (Abs (x, _, t), Abs (y, _, u)) =
+ (case fast_string_ord (x, y) of EQUAL => comments_ord (t, u) | ord => ord)
+ | comments_ord (t1 $ t2, u1 $ u2) =
+ (case comments_ord (t1, u1) of EQUAL => comments_ord (t2, u2) | ord => ord)
+ | comments_ord _ = EQUAL;
in
@@ -105,6 +111,9 @@
EQUAL => (case atoms_ord tu of EQUAL => types_ord tu | ord => ord)
| ord => ord);
+fun syntax_term_ord tu =
+ (case fast_term_ord tu of EQUAL => comments_ord tu | ord => ord);
+
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/term_sharing.ML Thu Jul 14 22:53:43 2011 +0200
@@ -0,0 +1,66 @@
+(* Title: Pure/term_sharing.ML
+ Author: Makarius
+
+Local sharing of type/term sub-structure, with global interning of
+formal entity names.
+*)
+
+signature TERM_SHARING =
+sig
+ val init: theory -> (typ -> typ) * (term -> term)
+ val typs: theory -> typ list -> typ list
+ val terms: theory -> term list -> term list
+end;
+
+structure Term_Sharing: TERM_SHARING =
+struct
+
+structure Syntax_Termtab = Table(type key = term val ord = Term_Ord.syntax_term_ord);
+
+fun init thy =
+ let
+ val {classes = (_, algebra), types = (_, types), ...} = Type.rep_tsig (Sign.tsig_of thy);
+
+ val sort = perhaps (try (Sorts.certify_sort algebra));
+ val tycon = perhaps (Option.map #1 o Symtab.lookup_key types);
+ val const = perhaps (try (#1 o Consts.the_const (Sign.consts_of thy)));
+
+ val typs = Unsynchronized.ref (Typtab.empty: unit Typtab.table);
+ val terms = Unsynchronized.ref (Syntax_Termtab.empty: unit Syntax_Termtab.table);
+
+ fun typ T =
+ (case Typtab.lookup_key (! typs) T of
+ SOME (T', ()) => T'
+ | NONE =>
+ let
+ val T' =
+ (case T of
+ Type (a, Ts) => Type (tycon a, map typ Ts)
+ | TFree (a, S) => TFree (a, sort S)
+ | TVar (a, S) => TVar (a, sort S));
+ val _ = Unsynchronized.change typs (Typtab.update (T', ()));
+ in T' end);
+
+ fun term tm =
+ (case Syntax_Termtab.lookup_key (! terms) tm of
+ SOME (tm', ()) => tm'
+ | NONE =>
+ let
+ val tm' =
+ (case tm of
+ Const (c, T) => Const (const c, typ T)
+ | Free (x, T) => Free (x, typ T)
+ | Var (xi, T) => Var (xi, typ T)
+ | Bound i => Bound i
+ | Abs (x, T, t) => Abs (x, typ T, term t)
+ | t $ u => term t $ term u);
+ val _ = Unsynchronized.change terms (Syntax_Termtab.update (tm', ()));
+ in tm' end);
+
+ in (typ, term) end;
+
+val typs = map o #1 o init;
+val terms = map o #2 o init;
+
+end;
+
--- a/src/Pure/thm.ML Thu Jul 14 22:08:11 2011 +0200
+++ b/src/Pure/thm.ML Thu Jul 14 22:53:43 2011 +0200
@@ -106,6 +106,7 @@
val axioms_of: theory -> (string * thm) list
val get_tags: thm -> Properties.T
val map_tags: (Properties.T -> Properties.T) -> thm -> thm
+ val compress: thm -> thm
val norm_proof: thm -> thm
val adjust_maxidx_thm: int -> thm -> thm
(*meta rules*)
@@ -630,6 +631,26 @@
shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop});
+(* technical adjustments *)
+
+fun compress (Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =
+ let
+ val thy = Theory.deref thy_ref;
+ val term = #2 (Term_Sharing.init thy);
+ val hyps' = map term hyps;
+ val tpairs' = map (pairself term) tpairs;
+ val prop' = term prop;
+ in
+ Thm (der,
+ {thy_ref = Theory.check_thy thy,
+ tags = tags,
+ maxidx = maxidx,
+ shyps = shyps,
+ hyps = hyps',
+ tpairs = tpairs',
+ prop = prop'})
+ end;
+
fun norm_proof (Thm (der, args as {thy_ref, ...})) =
let
val thy = Theory.deref thy_ref;