src/HOL/Tools/typedef.ML

--- a/src/HOL/Tools/typedef.ML	Sun Apr 11 14:06:35 2010 +0200
+++ b/src/HOL/Tools/typedef.ML	Sun Apr 11 14:30:34 2010 +0200
@@ -117,7 +117,7 @@
 
     val typedef_deps = Term.add_consts A [];
 
-    val (axiom, axiom_thy) = consts_thy
+    val ((axiom_name, axiom), axiom_thy) = consts_thy
       |> Thm.add_axiom (typedef_name, mk_typedef newT oldT RepC AbsC A)
       ||> Theory.add_deps "" (dest_Const RepC) typedef_deps
       ||> Theory.add_deps "" (dest_Const AbsC) typedef_deps;