defensive Term_Sharing, to avoid extending trusted code base of inference kernel;

--- a/src/Pure/term_sharing.ML	Sat Jul 23 20:11:18 2011 +0200
+++ b/src/Pure/term_sharing.ML	Sat Jul 23 20:34:33 2011 +0200
@@ -57,7 +57,13 @@
             val _ = Unsynchronized.change terms (Syntax_Termtab.update (tm', ()));
           in tm' end);
 
-  in (typ, term) end;
+    fun check eq f x =
+      let val x' = f x in
+        if eq (x, x') then x'
+        else raise Fail "Something is utterly wrong"
+      end;
+
+  in (check (op =) typ, check (op =) term) end;
 
 val typs = map o #1 o init;
 val terms = map o #2 o init;