equal
deleted
inserted
replaced
131 val allE_Nil = read_instantiate_sg (the_context()) [("x", "[]")] allE; |
131 val allE_Nil = read_instantiate_sg (the_context()) [("x", "[]")] allE; |
132 |
132 |
133 val meta_spec = thm "meta_spec"; |
133 val meta_spec = thm "meta_spec"; |
134 |
134 |
135 fun projections rule = |
135 fun projections rule = |
136 ProjectRule.projections rule |
136 ProjectRule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule |
137 |> map (standard #> RuleCases.save rule); |
137 |> map (standard #> RuleCases.save rule); |
138 |
138 |
139 fun gen_add_nominal_datatype prep_typ err flat_names new_type_names dts thy = |
139 fun gen_add_nominal_datatype prep_typ err flat_names new_type_names dts thy = |
140 let |
140 let |
141 (* this theory is used just for parsing *) |
141 (* this theory is used just for parsing *) |