src/HOL/Tools/float_syntax.ML
changeset 46236 ae79f2978a67
parent 42290 b1f544c84040
child 47108 2a1953f0d20d
     1.1 --- a/src/HOL/Tools/float_syntax.ML	Mon Jan 16 20:32:33 2012 +0100
     1.2 +++ b/src/HOL/Tools/float_syntax.ML	Mon Jan 16 21:50:15 2012 +0100
     1.3 @@ -35,8 +35,9 @@
     1.4  
     1.5  in
     1.6  
     1.7 -fun float_tr (*"_Float"*) [t as Const (str, _)] = mk_frac str
     1.8 -  | float_tr (*"_Float"*) ts = raise TERM ("float_tr", ts);
     1.9 +fun float_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ float_tr [t] $ u
    1.10 +  | float_tr [t as Const (str, _)] = mk_frac str
    1.11 +  | float_tr ts = raise TERM ("float_tr", ts);
    1.12  
    1.13  end;
    1.14