src/Pure/Isar/class_declaration.ML
changeset 38493 95a41e6ef5a8
parent 38435 1e1ef69ec0de
child 38756 d07959fabde6
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Tue Aug 17 14:33:44 2010 +0200
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Tue Aug 17 17:54:46 2010 +0200
     1.3 @@ -129,18 +129,22 @@
     1.4                    ^ Syntax.string_of_sort_global thy a_sort ^ ".")
     1.5              | _ => error "Multiple type variables in class specification.";
     1.6        in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end;
     1.7 +    val after_infer_fixate = (map o map_atyps)
     1.8 +      (fn T as TFree _ => T | T as TVar (vi, sort) =>
     1.9 +        if Type_Infer.is_param vi then Type_Infer.param 0 (Name.aT, sort) else T);
    1.10      fun add_typ_check level name f = Context.proof_map
    1.11        (Syntax.add_typ_check level name (fn Ts => fn ctxt =>
    1.12          let val Ts' = f Ts in if eq_list (op =) (Ts, Ts') then NONE else SOME (Ts', ctxt) end));
    1.13  
    1.14      (* preprocessing elements, retrieving base sort from type-checked elements *)
    1.15 +    val raw_supexpr = (map (fn sup => (sup, (("", false),
    1.16 +      Expression.Positional []))) sups, []);
    1.17      val init_class_body = fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints
    1.18        #> Class.redeclare_operations thy sups
    1.19        #> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc
    1.20        #> add_typ_check ~10 "singleton_fixate" singleton_fixate;
    1.21 -    val raw_supexpr = (map (fn sup => (sup, (("", false),
    1.22 -      Expression.Positional []))) sups, []);
    1.23      val ((raw_supparams, _, raw_inferred_elems), _) = ProofContext.init_global thy
    1.24 +      |> add_typ_check 5 "after_infer_fixate" after_infer_fixate
    1.25        |> prep_decl raw_supexpr init_class_body raw_elems;
    1.26      fun filter_element (Element.Fixes []) = NONE
    1.27        | filter_element (e as Element.Fixes _) = SOME e