equal
deleted
inserted
replaced
97 let |
97 let |
98 val ctxt = Proof_Context.init_global thy |> Variable.declare_typ repT; |
98 val ctxt = Proof_Context.init_global thy |> Variable.declare_typ repT; |
99 val vs = map (Proof_Context.check_tfree ctxt) raw_vs; |
99 val vs = map (Proof_Context.check_tfree ctxt) raw_vs; |
100 in |
100 in |
101 thy |
101 thy |
102 |> Typedef.add_typedef_global false (raw_tyco, vs, NoSyn) |
102 |> Typedef.add_typedef_global (raw_tyco, vs, NoSyn) |
103 (HOLogic.mk_UNIV repT) NONE (fn ctxt' => resolve_tac ctxt' [UNIV_witness] 1) |
103 (HOLogic.mk_UNIV repT) NONE (fn ctxt' => resolve_tac ctxt' [UNIV_witness] 1) |
104 |-> (fn (tyco, info) => get_typedef_info tyco vs info) |
104 |-> (fn (tyco, info) => get_typedef_info tyco vs info) |
105 end; |
105 end; |
106 |
106 |
107 fun mk_cons_tuple (left, right) = |
107 fun mk_cons_tuple (left, right) = |