src/Pure/sign.ML
changeset 25117 74b279146ecb
parent 25071 6680bebdfc28
child 25323 50d4c8257d06
     1.1 --- a/src/Pure/sign.ML	Sat Oct 20 18:54:29 2007 +0200
     1.2 +++ b/src/Pure/sign.ML	Sat Oct 20 18:54:30 2007 +0200
     1.3 @@ -442,9 +442,9 @@
     1.4  fun no_variables kind add addT mk mkT pp tm =
     1.5    (case (add tm [], addT tm []) of
     1.6      ([], []) => tm
     1.7 -  | (frees, tfrees) => error (Pretty.string_of (Pretty.block (Pretty.breaks
     1.8 -      (Pretty.str ("Illegal " ^ kind ^ " variable(s) in term:") ::
     1.9 -       map (Pretty.term pp o mk) frees @ map (Pretty.typ pp o mkT) tfrees)))));
    1.10 +  | (frees, tfrees) => error (Pretty.string_of (Pretty.block
    1.11 +      (Pretty.str ("Illegal " ^ kind ^ " variable(s) in term:") :: Pretty.brk 1 ::
    1.12 +       Pretty.commas (map (Pretty.term pp o mk) frees @ map (Pretty.typ pp o mkT) tfrees)))));
    1.13  
    1.14  val no_frees = no_variables "free" Term.add_frees Term.add_tfrees Free TFree;
    1.15  val no_vars = no_variables "schematic" Term.add_vars Term.add_tvars Var TVar;