sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML);
minor tuning;

--- a/src/Pure/IsaMakefile	Wed Jul 13 20:13:27 2011 +0200
+++ b/src/Pure/IsaMakefile	Wed Jul 13 20:36:18 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/proof_context.ML	Wed Jul 13 20:13:27 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Jul 13 20:36:18 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/ml_antiquote.ML	Wed Jul 13 20:13:27 2011 +0200
+++ b/src/Pure/ML/ml_antiquote.ML	Wed Jul 13 20:36:18 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	Wed Jul 13 20:13:27 2011 +0200
+++ b/src/Pure/ROOT.ML	Wed Jul 13 20:36:18 2011 +0200
@@ -146,6 +146,7 @@
 use "interpretation.ML";
 use "proofterm.ML";
 use "thm.ML";
+use "term_sharing.ML";
 use "more_thm.ML";
 use "facts.ML";
 use "global_theory.ML";

--- a/src/Pure/Syntax/syntax_phases.ML	Wed Jul 13 20:13:27 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Jul 13 20:36:18 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	Wed Jul 13 20:13:27 2011 +0200
+++ b/src/Pure/consts.ML	Wed Jul 13 20:36:18 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/sign.ML	Wed Jul 13 20:13:27 2011 +0200
+++ b/src/Pure/sign.ML	Wed Jul 13 20:36:18 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/term_ord.ML	Wed Jul 13 20:13:27 2011 +0200
+++ b/src/Pure/term_ord.ML	Wed Jul 13 20:36:18 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;