src/Pure/sign.ML
changeset 1458 fd510875fb71
parent 1414 036e072b215a
child 1460 5a6f2aabd538
     1.1 --- a/src/Pure/sign.ML	Mon Jan 29 13:50:10 1996 +0100
     1.2 +++ b/src/Pure/sign.ML	Mon Jan 29 13:56:41 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;