# HG changeset patch
# User wenzelm
# Date 1310676823 -7200
# Node ID 1162191cb57c203cca561cb559192a4b3d6d3645
# Parent  6ce89c4ec14197dfbc8484142b39c463d7a9765f# Parent  fad7758421bf07d72a9bd6876ce2dcf07d83ec80
merged

diff -r 6ce89c4ec141 -r 1162191cb57c src/Pure/Concurrent/task_queue.ML
--- 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)
diff -r 6ce89c4ec141 -r 1162191cb57c src/Pure/General/graph.ML
--- 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
diff -r 6ce89c4ec141 -r 1162191cb57c src/Pure/General/markup.ML
--- 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;
 
diff -r 6ce89c4ec141 -r 1162191cb57c src/Pure/General/table.ML
--- 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
diff -r 6ce89c4ec141 -r 1162191cb57c src/Pure/General/xml.ML
--- 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
diff -r 6ce89c4ec141 -r 1162191cb57c src/Pure/IsaMakefile
--- 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						\
diff -r 6ce89c4ec141 -r 1162191cb57c src/Pure/Isar/generic_target.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) =
diff -r 6ce89c4ec141 -r 1162191cb57c src/Pure/Isar/proof_context.ML
--- 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;
diff -r 6ce89c4ec141 -r 1162191cb57c src/Pure/ML/install_pp_polyml-5.3.ML
--- 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));
 
diff -r 6ce89c4ec141 -r 1162191cb57c src/Pure/ML/ml_antiquote.ML
--- 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")
diff -r 6ce89c4ec141 -r 1162191cb57c src/Pure/ROOT.ML
--- 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";
diff -r 6ce89c4ec141 -r 1162191cb57c src/Pure/Syntax/syntax_phases.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;
diff -r 6ce89c4ec141 -r 1162191cb57c src/Pure/consts.ML
--- 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)));
diff -r 6ce89c4ec141 -r 1162191cb57c src/Pure/library.ML
--- 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
diff -r 6ce89c4ec141 -r 1162191cb57c src/Pure/proofterm.ML
--- 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 =
diff -r 6ce89c4ec141 -r 1162191cb57c src/Pure/pure_setup.ML
--- 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";
diff -r 6ce89c4ec141 -r 1162191cb57c src/Pure/sign.ML
--- 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;
diff -r 6ce89c4ec141 -r 1162191cb57c src/Pure/sorts.ML
--- 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);
 
diff -r 6ce89c4ec141 -r 1162191cb57c src/Pure/term_ord.ML
--- 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;
 
 
diff -r 6ce89c4ec141 -r 1162191cb57c src/Pure/term_sharing.ML
--- /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;
+
diff -r 6ce89c4ec141 -r 1162191cb57c src/Pure/thm.ML
--- 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;