equal
deleted
inserted
replaced
974 (*WN110613 fun declare_constraints' shall replace fun declare_constraints*) |
974 (*WN110613 fun declare_constraints' shall replace fun declare_constraints*) |
975 fun declare_constraints t ctxt = |
975 fun declare_constraints t ctxt = |
976 let |
976 let |
977 fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of |
977 fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of |
978 (_, _::_) => (Free (v,T)::get_vars vs) |
978 (_, _::_) => (Free (v,T)::get_vars vs) |
979 | (_, [] ) => get_vars vs) (*filter out nums as long as *) |
979 | (_, [] ) => get_vars vs) (*filter out nums as long as |
|
980 we have Free ("123",_)*) |
980 | get_vars [] = []; |
981 | get_vars [] = []; |
981 val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars; |
982 val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars; |
982 in fold Variable.declare_constraints ts ctxt end; |
983 in fold Variable.declare_constraints ts ctxt end; |
983 |
984 |
984 datatype Isac_Ctxt = |
985 datatype Isac_Ctxt = |