changeset 43950 | 49f0e4ae2350 |
parent 43796 | 7293403dc38b |
child 45595 | fe57d786fd5b |
--- 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;