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