1.1 --- a/src/HOL/Import/proof_kernel.ML	Tue Mar 14 22:06:29 2006 +0100
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Tue Mar 14 22:06:31 2006 +0100
     1.3 @@ -183,6 +183,8 @@
     1.4  
     1.5  (* Compatibility. *)
     1.6  
     1.7 +val string_of_mixfix = Pretty.string_of o Syntax.pretty_mixfix;
     1.8 +
     1.9  fun mk_syn thy c =
    1.10    if Syntax.is_identifier c andalso not (Syntax.is_keyword (Sign.syn_of thy) c) then NoSyn
    1.11    else Syntax.literal c
    1.12 @@ -289,7 +291,6 @@
    1.13    | implode_subst (x::r::rest) = ((x,r)::(implode_subst rest))
    1.14    | implode_subst _ = raise ERR "implode_subst" "malformed substitution list"
    1.15  
    1.16 -fun apboth f (x,y) = (f x,f y)
    1.17  end
    1.18  open Lib
    1.19  
    1.20 @@ -1240,7 +1241,7 @@
    1.21      let
    1.22  	val sub = Substring.full str
    1.23  	val (f,idx) = apsnd Substring.string (Substring.splitr Char.isDigit sub)
    1.24 -	val (newstr,u) = apboth Substring.string (Substring.splitr (fn c => c = #"_") f)
    1.25 +	val (newstr,u) = pairself Substring.string (Substring.splitr (fn c => c = #"_") f)
    1.26      in
    1.27  	if not (idx = "") andalso u = "_"
    1.28  	then SOME (newstr,valOf(Int.fromString idx))
    1.29 @@ -1944,14 +1945,14 @@
    1.30  			let
    1.31  			    val p1 = quotename constname
    1.32  			    val p2 = string_of_ctyp (ctyp_of thy'' ctype)
    1.33 -			    val p3 = Syntax.string_of_mixfix csyn
    1.34 +			    val p3 = string_of_mixfix csyn
    1.35  			    val p4 = smart_string_of_cterm crhs
    1.36  			in
    1.37  			    add_dump ("constdefs\n  " ^p1^ " :: \"" ^p2^ "\" "^p3^ "\n  " ^p4) thy''  
    1.38  			end
    1.39  		    else
    1.40  			(add_dump ("consts\n  " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy'' ctype) ^
    1.41 -				   "\" " ^ (Syntax.string_of_mixfix csyn) ^ "\n\ndefs\n  " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs))
    1.42 +				   "\" " ^ (string_of_mixfix csyn) ^ "\n\ndefs\n  " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs))
    1.43  				  thy'')
    1.44  	val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of
    1.45  		      SOME (_,res) => HOLThm(rens_of linfo,res)
    1.46 @@ -2013,7 +2014,7 @@
    1.47  							      ((cname,cT,mk_syn thy cname)::cs,p)
    1.48  							  end) (([],HOLogic.dest_Trueprop (concl_of th)),names)
    1.49  			       val str = Library.foldl (fn (acc,(c,T,csyn)) =>
    1.50 -						   acc ^ "\n  " ^ (quotename c) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy T) ^ "\" " ^ (Syntax.string_of_mixfix csyn)) ("consts",consts)
    1.51 +						   acc ^ "\n  " ^ (quotename c) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy T) ^ "\" " ^ (string_of_mixfix csyn)) ("consts",consts)
    1.52  			       val thy' = add_dump str thy
    1.53  			       val _ = ImportRecorder.add_consts consts
    1.54  			   in
    1.55 @@ -2125,7 +2126,7 @@
    1.56  			    then smart_string_of_cterm
    1.57  			    else Library.setmp show_all_types true smart_string_of_cterm
    1.58  	    val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " 
    1.59 -				 ^ (Syntax.string_of_mixfix tsyn) ^ "\n  by (rule typedef_helper,import " ^ thyname ^ " " ^ thmname ^ ")") thy4
    1.60 +				 ^ (string_of_mixfix tsyn) ^ "\n  by (rule typedef_helper,import " ^ thyname ^ " " ^ thmname ^ ")") thy4
    1.61  	    
    1.62  	    val thy6 = add_dump ("lemmas " ^ thmname ^ " = typedef_hol2hol4 [OF type_definition_" ^ tycname ^ "]") thy5
    1.63                
    1.64 @@ -2140,7 +2141,7 @@
    1.65      let
    1.66  	val n = quotename constname
    1.67  	val t = string_of_ctyp (ctyp_of thy ty)
    1.68 -	val syn = Syntax.string_of_mixfix (mk_syn thy constname)
    1.69 +	val syn = string_of_mixfix (mk_syn thy constname)
    1.70  	(*val eq = smart_string_of_cterm (cterm_of thy (Const(rhs, ty)))*)
    1.71          val eq = quote (constname ^ " == "^rhs)
    1.72  	val d = case defname of NONE => "" | SOME defname => (quotename defname)^" : "
    1.73 @@ -2151,7 +2152,7 @@
    1.74  fun add_dump_syntax thy name = 
    1.75      let
    1.76        val n = quotename name
    1.77 -      val syn = Syntax.string_of_mixfix (mk_syn thy name)
    1.78 +      val syn = string_of_mixfix (mk_syn thy name)
    1.79      in
    1.80        add_dump ("syntax\n  "^n^" :: _ "^syn) thy
    1.81      end
    1.82 @@ -2224,7 +2225,7 @@
    1.83  			    else Library.setmp show_all_types true smart_string_of_cterm
    1.84  	    val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ 
    1.85                " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " ^ 
    1.86 -	      (Syntax.string_of_mixfix tsyn) ^ " morphisms "^
    1.87 +	      (string_of_mixfix tsyn) ^ " morphisms "^
    1.88                (quote rep_name)^" "^(quote abs_name)^"\n"^ 
    1.89  	      ("  apply (rule light_ex_imp_nonempty[where t="^
    1.90                (proc_prop (cterm_of thy4 t))^"])\n"^