Sorts.str_of_sort;
authorwenzelm
Wed Apr 16 18:22:10 1997 +0200 (1997-04-16)
changeset 296297ae96c72d8c
parent 2961 842be30dc336
child 2963 f3b5af1c5a67
Sorts.str_of_sort;
src/Pure/goals.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/goals.ML	Wed Apr 16 18:21:00 1997 +0200
     1.2 +++ b/src/Pure/goals.ML	Wed Apr 16 18:22:10 1997 +0200
     1.3 @@ -154,7 +154,7 @@
     1.4                   cat_lines (map (Sign.string_of_term sign) hyps))
     1.5  	    else if not (null xshyps) then !result_error_ref state
     1.6                  ("Extra sort hypotheses: " ^
     1.7 -                 commas (map Type.str_of_sort xshyps))
     1.8 +                 commas (map Sorts.str_of_sort xshyps))
     1.9  	    else if Pattern.matches (#tsig(Sign.rep_sg sign)) 
    1.10  			            (term_of chorn, prop)
    1.11  		 then  standard th 
     2.1 --- a/src/Pure/thm.ML	Wed Apr 16 18:21:00 1997 +0200
     2.2 +++ b/src/Pure/thm.ML	Wed Apr 16 18:22:10 1997 +0200
     2.3 @@ -502,7 +502,7 @@
     2.4               not (!force_strip_shyps) then shyps'
     2.5            else    (* FIXME tmp *)
     2.6                (warning ("Removed sort hypotheses: " ^
     2.7 -                        commas (map Type.str_of_sort (shyps' \\ sorts)));
     2.8 +                        commas (map Sorts.str_of_sort (shyps' \\ sorts)));
     2.9                 warning "Let's hope these sorts are non-empty!";
    2.10             sorts)),
    2.11        hyps = hyps,