src/ZF/ind_syntax.ML
changeset 27261 5b3101338f42
parent 27239 f2f42f9fa09d
child 28965 1de908189869
     1.1 --- a/src/ZF/ind_syntax.ML	Wed Jun 18 18:55:08 2008 +0200
     1.2 +++ b/src/ZF/ind_syntax.ML	Wed Jun 18 18:55:10 2008 +0200
     1.3 @@ -66,8 +66,9 @@
     1.4    | dest_mem _ = error "Constructor specifications must have the form x:A";
     1.5  
     1.6  (*read a constructor specification*)
     1.7 -fun read_construct sign (id, sprems, syn) =
     1.8 -    let val prems = map (Sign.simple_read_term sign FOLogic.oT) sprems
     1.9 +fun read_construct ctxt (id, sprems, syn) =
    1.10 +    let val prems = map (Syntax.parse_term ctxt #> TypeInfer.constrain FOLogic.oT) sprems
    1.11 +          |> Syntax.check_terms ctxt
    1.12          val args = map (#1 o dest_mem) prems
    1.13          val T = (map (#2 o dest_Free) args) ---> iT
    1.14                  handle TERM _ => error