src/HOL/Import/proof_kernel.ML

 	  | G 1 = Library.setmp show_types true
 	  | G 2 = Library.setmp show_all_types true
 	  | G _ = error ("ProofKernel.smart_string_of_cterm internal error: " ^ (G 2 string_of_cterm ct))
 	fun F sh_br n =
 	    let
-		val str = Library.setmp show_brackets sh_br (G n (Output.output o string_of_cterm)) ct
+		val str = Library.setmp show_brackets sh_br (G n string_of_cterm) ct
 		val cu  = transform_error (read_cterm sign) (str,T)
 	    in
 		if match cu
 		then quote str
 		else F false (n+1)

 	transform_error (Library.setmp Syntax.ambiguity_is_error true (F false)) 0
     end
     handle ERROR_MESSAGE mesg =>
 	   (writeln "Exception in smart_string_of_cterm!";
 	    writeln mesg;
-	    quote (Output.output (string_of_cterm ct)))
+	    quote (string_of_cterm ct))
 
 val smart_string_of_thm = smart_string_of_cterm o cprop_of
 
 fun prth th = writeln ((Library.setmp print_mode [] string_of_thm) th)
 fun prc ct = writeln ((Library.setmp print_mode [] string_of_cterm) ct)

 	val sg = sign_of thy''
 	val rew = rewrite_hol4_term eq thy''
 	val crhs = cterm_of sg (#2 (Logic.dest_equals (prop_of rew)))
 	val thy22 = if (def_name constname) = thmname andalso not redeclared andalso csyn = NoSyn
 		    then
-			add_dump ("constdefs\n  " ^ (quotename constname) ^ " :: \"" ^ Output.output (string_of_ctyp (ctyp_of sg ctype)) ^ "\" " ^ (Syntax.string_of_mixfix csyn) ^ "\n  " ^ (smart_string_of_cterm crhs)) thy''
+			add_dump ("constdefs\n  " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of sg ctype) ^ "\" " ^ (Syntax.string_of_mixfix csyn) ^ "\n  " ^ (smart_string_of_cterm crhs)) thy''
 		    else
-			add_dump ("consts\n  " ^ (quotename constname) ^ " :: \"" ^ Output.output (string_of_ctyp (ctyp_of sg ctype)) ^
+			add_dump ("consts\n  " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of sg ctype) ^
 				  "\" " ^ (Syntax.string_of_mixfix csyn) ^ "\n\ndefs\n  " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs))
 				 thy''
 
 	val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of
 		     Some (_,res) => HOLThm(rens_of linfo,res)

 							  in
 							      ((cname,cT,mk_syn thy cname)::cs,p)
 							  end) (([],HOLogic.dest_Trueprop (concl_of th)),names)
 			       val sg = sign_of thy
 			       val str = foldl (fn (acc,(c,T,csyn)) =>
-						   acc ^ "\n  " ^ (quotename c) ^ " :: \"" ^ Output.output (string_of_ctyp (ctyp_of sg T)) ^ "\" " ^ (Syntax.string_of_mixfix csyn)) ("consts",consts)
+						   acc ^ "\n  " ^ (quotename c) ^ " :: \"" ^ string_of_ctyp (ctyp_of sg T) ^ "\" " ^ (Syntax.string_of_mixfix csyn)) ("consts",consts)
 			       val thy' = add_dump str thy
 			   in
 			       Theory.add_consts_i consts thy'
 			   end