--- a/src/HOL/Import/proof_kernel.ML Thu Oct 15 15:53:33 2009 +0200
+++ b/src/HOL/Import/proof_kernel.ML Thu Oct 15 16:15:22 2009 +0200
@@ -2177,7 +2177,7 @@
_ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c
| _ => raise ERR "type_introduction" "Bad type definition theorem"
val tfrees = OldTerm.term_tfrees c
- val tnames = sort string_ord (map fst tfrees)
+ val tnames = sort_strings (map fst tfrees)
val tsyn = mk_syn thy tycname
val typ = (tycname,tnames,tsyn)
val ((_, typedef_info), thy') =