equal
deleted
inserted
replaced
64 fun dest_mem (Const (@{const_name mem}, _) $ x $ A) = (x, A) |
64 fun dest_mem (Const (@{const_name mem}, _) $ x $ A) = (x, A) |
65 | dest_mem _ = error "Constructor specifications must have the form x:A"; |
65 | dest_mem _ = error "Constructor specifications must have the form x:A"; |
66 |
66 |
67 (*read a constructor specification*) |
67 (*read a constructor specification*) |
68 fun read_construct ctxt (id: string, sprems, syn: mixfix) = |
68 fun read_construct ctxt (id: string, sprems, syn: mixfix) = |
69 let val prems = map (Syntax.parse_term ctxt #> TypeInfer.constrain FOLogic.oT) sprems |
69 let val prems = map (Syntax.parse_term ctxt #> Type_Infer.constrain FOLogic.oT) sprems |
70 |> Syntax.check_terms ctxt |
70 |> Syntax.check_terms ctxt |
71 val args = map (#1 o dest_mem) prems |
71 val args = map (#1 o dest_mem) prems |
72 val T = (map (#2 o dest_Free) args) ---> iT |
72 val T = (map (#2 o dest_Free) args) ---> iT |
73 handle TERM _ => error |
73 handle TERM _ => error |
74 "Bad variable in constructor specification" |
74 "Bad variable in constructor specification" |