src/HOL/Import/proof_kernel.ML
changeset 32945 63db9da65a19
parent 32740 9dd0a2f83429
child 32951 83392f9d303f
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Thu Oct 15 15:53:33 2009 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Oct 15 16:15:22 2009 +0200
     1.3 @@ -2177,7 +2177,7 @@
     1.4                          _ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c
     1.5                        | _ => raise ERR "type_introduction" "Bad type definition theorem"
     1.6              val tfrees = OldTerm.term_tfrees c
     1.7 -            val tnames = sort string_ord (map fst tfrees)
     1.8 +            val tnames = sort_strings (map fst tfrees)
     1.9              val tsyn = mk_syn thy tycname
    1.10              val typ = (tycname,tnames,tsyn)
    1.11              val ((_, typedef_info), thy') =