src/Pure/sign.ML
changeset 20330 6192478fdba5
parent 20230 04cb2d917de5
child 20548 8ef25fe585a8
     1.1 --- a/src/Pure/sign.ML	Thu Aug 03 17:30:37 2006 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Aug 03 17:30:38 2006 +0200
     1.3 @@ -481,11 +481,11 @@
     1.4  (* specifications *)
     1.5  
     1.6  fun no_vars pp tm =
     1.7 -  (case (Term.term_vars tm, Term.term_tvars tm) of
     1.8 +  (case (Term.add_vars tm [], Term.add_tvars tm []) of
     1.9      ([], []) => tm
    1.10 -  | (ts, ixns) => error (Pretty.string_of (Pretty.block (Pretty.breaks
    1.11 +  | (vars, tvars) => error (Pretty.string_of (Pretty.block (Pretty.breaks
    1.12        (Pretty.str "Illegal schematic variable(s) in term:" ::
    1.13 -       map (Pretty.term pp) ts @ map (Pretty.typ pp o TVar) ixns)))));
    1.14 +       map (Pretty.term pp o Var) vars @ map (Pretty.typ pp o TVar) tvars)))));
    1.15  
    1.16  fun cert_def pp tm =
    1.17    let val ((lhs, rhs), _) = tm