1.1 --- a/src/Pure/term_sharing.ML	Sat Jul 23 20:11:18 2011 +0200
     1.2 +++ b/src/Pure/term_sharing.ML	Sat Jul 23 20:34:33 2011 +0200
     1.3 @@ -57,7 +57,13 @@
     1.4              val _ = Unsynchronized.change terms (Syntax_Termtab.update (tm', ()));
     1.5            in tm' end);
     1.6  
     1.7 -  in (typ, term) end;
     1.8 +    fun check eq f x =
     1.9 +      let val x' = f x in
    1.10 +        if eq (x, x') then x'
    1.11 +        else raise Fail "Something is utterly wrong"
    1.12 +      end;
    1.13 +
    1.14 +  in (check (op =) typ, check (op =) term) end;
    1.15  
    1.16  val typs = map o #1 o init;
    1.17  val terms = map o #2 o init;