src/Pure/sign.ML
changeset 1460 5a6f2aabd538
parent 1458 fd510875fb71
child 1494 22f67e796445
     1.1 --- a/src/Pure/sign.ML	Mon Jan 29 13:58:15 1996 +0100
     1.2 +++ b/src/Pure/sign.ML	Mon Jan 29 14:16:13 1996 +0100
     1.3 @@ -266,13 +266,13 @@
     1.4  (*Package error messages from type checking*)
     1.5  fun exn_type_msg sg (msg, Ts, ts) =
     1.6      let val show_typ = string_of_typ sg
     1.7 -        val show_term = string_of_term sg
     1.8 -        fun term_err [] = ""
     1.9 -          | term_err [t] = "\nInvolving this term:\n" ^ show_term t
    1.10 -          | term_err ts =
    1.11 -            "\nInvolving these terms:\n" ^ cat_lines (map show_term ts);
    1.12 +	val show_term = string_of_term sg
    1.13 +	fun term_err [] = ""
    1.14 +	  | term_err [t] = "\nInvolving this term:\n" ^ show_term t
    1.15 +	  | term_err ts =
    1.16 +	    "\nInvolving these terms:\n" ^ cat_lines (map show_term ts);
    1.17      in  "\nType checking error: " ^ msg ^ "\n" ^
    1.18 -        cat_lines (map show_typ Ts) ^ term_err ts ^ "\n"
    1.19 +	cat_lines (map show_typ Ts) ^ term_err ts ^ "\n"
    1.20      end; 
    1.21  
    1.22  
    1.23 @@ -308,7 +308,7 @@
    1.24  
    1.25      fun process_term(res,(t,i)) =
    1.26         let val ([u],tye) = 
    1.27 -               Type.infer_types(tsig,ct,types,sorts,used,freeze,[T'],[t])
    1.28 +	       Type.infer_types(tsig,ct,types,sorts,used,freeze,[T'],[t])
    1.29         in case res of
    1.30              One(_,t0,_) => Ambigs([u,t0])
    1.31            | Errs _ => One(i,u,tye)
    1.32 @@ -406,9 +406,9 @@
    1.33  fun ext_cnsts rd_const syn_only (syn, tsig, ctab) raw_consts =
    1.34    let
    1.35      fun prep_const (c, ty, mx) = 
    1.36 -          (c, 
    1.37 -           compress_type (varifyT (cert_typ tsig (no_tvars ty))), 
    1.38 -           mx)
    1.39 +	  (c, 
    1.40 +	   compress_type (varifyT (cert_typ tsig (no_tvars ty))), 
    1.41 +	   mx)
    1.42        handle TYPE (msg, _, _) => (writeln msg; err_in_const (Syntax.const_name c mx));
    1.43  
    1.44      val consts = map (prep_const o rd_const syn tsig) raw_consts;