equal
deleted
inserted
replaced
145 apply(clarify) |
145 apply(clarify) |
146 apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff) |
146 apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff) |
147 apply auto |
147 apply auto |
148 done |
148 done |
149 |
149 |
|
150 (* PROBLEM: |
|
151 Type schemes with separate datatypes |
|
152 |
|
153 nominal_datatype T = |
|
154 TVar "name" |
|
155 | TFun "T" "T" |
|
156 nominal_datatype TyS = |
|
157 TAll xs::"name list" ty::"T" bind xs in ty |
|
158 |
|
159 *** exception Datatype raised |
|
160 *** (line 218 of "/usr/local/src/Isabelle_16-Mar-2010/src/HOL/Tools/Datatype/datatype_aux.ML") |
|
161 *** At command "nominal_datatype". |
|
162 *) |
|
163 |
|
164 |
150 end |
165 end |