src/Tools/isac/Interpret/mstools.sml
branchdecompose-isar
changeset 42272 dcc5d2601cf7
parent 42023 927cb6806af1
child 42394 977788dfed26
     1.1 --- a/src/Tools/isac/Interpret/mstools.sml	Tue Sep 13 10:51:56 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/mstools.sml	Sun Sep 18 15:21:46 2011 +0200
     1.3 @@ -976,7 +976,8 @@
     1.4      let
     1.5        fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of
     1.6                (_, _::_) => (Free (v,T)::get_vars vs)
     1.7 -            | (_, []  ) => get_vars vs) (*filter out nums as long as *)
     1.8 +            | (_, []  ) => get_vars vs) (*filter out nums as long as 
     1.9 +                                          we have Free ("123",_)*)
    1.10          | get_vars [] = [];
    1.11        val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
    1.12      in fold Variable.declare_constraints ts ctxt end;