564 fun typedef_info thy s = |
564 fun typedef_info thy s = |
565 if is_frac_type thy (Type (s, [])) then |
565 if is_frac_type thy (Type (s, [])) then |
566 SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"}, |
566 SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"}, |
567 Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac}, |
567 Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac}, |
568 set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"} |
568 set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"} |
569 |> Logic.varify, |
569 |> Logic.varify_global, |
570 set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE} |
570 set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE} |
571 else case Typedef.get_info_global thy s of |
571 else case Typedef.get_info_global thy s of |
572 (* FIXME handle multiple typedef interpretations (!??) *) |
572 (* FIXME handle multiple typedef interpretations (!??) *) |
573 [{abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse, |
573 [{abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse, |
574 Rep_inverse, ...}] => |
574 Rep_inverse, ...}] => |
597 Same.commit (Envir.subst_type_same |
597 Same.commit (Envir.subst_type_same |
598 (Sign.typ_match thy (T1, T1') Vartab.empty)) T2 |
598 (Sign.typ_match thy (T1, T1') Vartab.empty)) T2 |
599 handle Type.TYPE_MATCH => |
599 handle Type.TYPE_MATCH => |
600 raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], []) |
600 raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], []) |
601 fun varify_and_instantiate_type thy T1 T1' T2 = |
601 fun varify_and_instantiate_type thy T1 T1' T2 = |
602 instantiate_type thy (Logic.varifyT T1) T1' (Logic.varifyT T2) |
602 instantiate_type thy (Logic.varifyT_global T1) T1' (Logic.varifyT_global T2) |
603 |
603 |
604 (* theory -> typ -> typ -> styp *) |
604 (* theory -> typ -> typ -> styp *) |
605 fun repair_constr_type thy body_T' T = |
605 fun repair_constr_type thy body_T' T = |
606 varify_and_instantiate_type thy (body_type T) body_T' T |
606 varify_and_instantiate_type thy (body_type T) body_T' T |
607 |
607 |