# HG changeset patch
# User wenzelm
# Date 1311446073 -7200
# Node ID 49f0e4ae23503c48c89a95f658d96b694ffb6d95
# Parent  94033767ef9becfa45b5ffd91164798bb209412e
defensive Term_Sharing, to avoid extending trusted code base of inference kernel;

diff -r 94033767ef9b -r 49f0e4ae2350 src/Pure/term_sharing.ML
--- 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;