changeset 37145 | 01aa36932739 |
parent 36945 | 9bec62c10714 |
child 38549 | d0385f2764d8 |
--- a/src/HOL/Tools/Function/function_core.ML Thu May 27 15:28:23 2010 +0200 +++ b/src/HOL/Tools/Function/function_core.ML Thu May 27 17:41:27 2010 +0200 @@ -879,7 +879,7 @@ val ranT = range_type fT val default = Syntax.parse_term lthy default_str - |> TypeInfer.constrain fT |> Syntax.check_term lthy + |> Type_Infer.constrain fT |> Syntax.check_term lthy val (globals, ctxt') = fix_globals domT ranT fvar lthy