src/ZF/ind_syntax.ML
changeset 37145 01aa36932739
parent 35129 ed24ba6f69aa
child 38514 bd9c4e8281ec
     1.1 --- a/src/ZF/ind_syntax.ML	Thu May 27 15:28:23 2010 +0200
     1.2 +++ b/src/ZF/ind_syntax.ML	Thu May 27 17:41:27 2010 +0200
     1.3 @@ -66,7 +66,7 @@
     1.4  
     1.5  (*read a constructor specification*)
     1.6  fun read_construct ctxt (id: string, sprems, syn: mixfix) =
     1.7 -    let val prems = map (Syntax.parse_term ctxt #> TypeInfer.constrain FOLogic.oT) sprems
     1.8 +    let val prems = map (Syntax.parse_term ctxt #> Type_Infer.constrain FOLogic.oT) sprems
     1.9            |> Syntax.check_terms ctxt
    1.10          val args = map (#1 o dest_mem) prems
    1.11          val T = (map (#2 o dest_Free) args) ---> iT