468 |
468 |
469 fun read_typ ctxt raw_T env = |
469 fun read_typ ctxt raw_T env = |
470 let |
470 let |
471 val ctxt' = fold (Variable.declare_typ o TFree) env ctxt; |
471 val ctxt' = fold (Variable.declare_typ o TFree) env ctxt; |
472 val T = Syntax.read_typ ctxt' raw_T; |
472 val T = Syntax.read_typ ctxt' raw_T; |
473 val env' = Misc_Legacy.add_typ_tfrees (T, env); |
473 val env' = Term.add_tfreesT T env; |
474 in (T, env') end; |
474 in (T, env') end; |
475 |
475 |
476 fun cert_typ ctxt raw_T env = |
476 fun cert_typ ctxt raw_T env = |
477 let |
477 let |
478 val thy = Proof_Context.theory_of ctxt; |
478 val thy = Proof_Context.theory_of ctxt; |
479 val T = Type.no_tvars (Sign.certify_typ thy raw_T) |
479 val T = Type.no_tvars (Sign.certify_typ thy raw_T) |
480 handle TYPE (msg, _, _) => error msg; |
480 handle TYPE (msg, _, _) => error msg; |
481 val env' = Misc_Legacy.add_typ_tfrees (T, env); |
481 val env' = Term.add_tfreesT T env; |
482 in (T, env') end; |
482 in (T, env') end; |
483 |
483 |
484 fun gen_define_statespace prep_typ state_space args name parents comps thy = |
484 fun gen_define_statespace prep_typ state_space args name parents comps thy = |
485 let (* - args distinct |
485 let (* - args distinct |
486 - only args may occur in comps and parent-instantiations |
486 - only args may occur in comps and parent-instantiations |