src/HOL/typedef.ML
changeset 2238 c72a23bbe762
parent 1475 7f5a4cd08209
child 2851 b6a5780e36b9
equal deleted inserted replaced
2237:f01ac387e82b 2238:c72a23bbe762
    78       mk_Trueprop (mk_eq (RepC $ (AbsC $ y_old), y_old)));
    78       mk_Trueprop (mk_eq (RepC $ (AbsC $ y_old), y_old)));
    79 
    79 
    80 
    80 
    81     (* errors *)
    81     (* errors *)
    82 
    82 
    83     val show_names = commas_quote o map fst;
    83     fun show_names pairs = commas_quote (map fst pairs);
    84 
    84 
    85     val illegal_vars =
    85     val illegal_vars =
    86       if null (term_vars set) andalso null (term_tvars set) then []
    86       if null (term_vars set) andalso null (term_tvars set) then []
    87       else ["Illegal schematic variable(s) on rhs"];
    87       else ["Illegal schematic variable(s) on rhs"];
    88 
    88