tuned
authorhaftmann
Wed Sep 10 14:58:01 2014 +0200 (2014-09-10)
changeset 582931d0343818ec0
parent 58292 e7320cceda9c
child 58294 7f990b3d5189
tuned
src/Pure/Isar/class_declaration.ML
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Wed Sep 10 14:57:03 2014 +0200
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Wed Sep 10 14:58:01 2014 +0200
     1.3 @@ -117,11 +117,11 @@
     1.4      val base_constraints = (map o apsnd)
     1.5        (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o snd)
     1.6          (Class.these_operations thy sups);
     1.7 -    fun singleton_fixate tms =
     1.8 +    fun singleton_fixate Ts =
     1.9        let
    1.10 -        val tfrees = fold Term.add_tfrees tms [];
    1.11 +        val tfrees = fold Term.add_tfreesT Ts [];
    1.12          val inferred_sort =
    1.13 -          (fold o fold_types o fold_atyps) (fn TVar (_, S) => inter_sort S | _ => I) tms [];
    1.14 +          (fold o fold_atyps) (fn TVar (_, S) => inter_sort S | _ => I) Ts [];
    1.15          val fixate_sort =
    1.16            (case tfrees of
    1.17              [] => inferred_sort
    1.18 @@ -137,20 +137,21 @@
    1.19            | _ => error "Multiple type variables in class specification");
    1.20          val fixateT = TFree (Name.aT, fixate_sort);
    1.21        in
    1.22 -        (map o map_types o map_atyps)
    1.23 -          (fn T as TVar (xi, _) => if Type_Infer.is_param xi then fixateT else T | T => T) tms
    1.24 +        (map o map_atyps)
    1.25 +          (fn T as TVar (xi, _) => if Type_Infer.is_param xi then fixateT else T | T => T) Ts
    1.26        end;
    1.27 -    fun after_infer_fixate tms =
    1.28 +    fun after_infer_fixate Ts =
    1.29        let
    1.30          val fixate_sort =
    1.31 -          (fold o fold_types o fold_atyps)
    1.32 -            (fn TVar (xi, S) => if Type_Infer.is_param xi then inter_sort S else I | _ => I) tms [];
    1.33 +          (fold o fold_atyps)
    1.34 +            (fn TVar (xi, S) => if Type_Infer.is_param xi then inter_sort S else I | _ => I) Ts [];
    1.35        in
    1.36 -        (map o map_types o map_atyps)
    1.37 +        (map o map_atyps)
    1.38            (fn T as TVar (xi, _) =>
    1.39                if Type_Infer.is_param xi then Type_Infer.param 0 (Name.aT, fixate_sort) else T
    1.40 -            | T => T) tms
    1.41 +            | T => T) Ts
    1.42        end;
    1.43 +    fun lift_check f _ ts = burrow_types f ts;
    1.44  
    1.45      (* preprocessing elements, retrieving base sort from type-checked elements *)
    1.46      val raw_supexpr =
    1.47 @@ -158,10 +159,10 @@
    1.48      val init_class_body =
    1.49        fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
    1.50        #> Class.redeclare_operations thy sups
    1.51 -      #> Context.proof_map (Syntax_Phases.term_check 0 "singleton_fixate" (K singleton_fixate));
    1.52 +      #> Context.proof_map (Syntax_Phases.term_check 0 "singleton_fixate" (lift_check singleton_fixate));
    1.53      val ((raw_supparams, _, raw_inferred_elems, _), _) =
    1.54        Proof_Context.init_global thy
    1.55 -      |> Context.proof_map (Syntax_Phases.term_check 0 "after_infer_fixate" (K after_infer_fixate))
    1.56 +      |> Context.proof_map (Syntax_Phases.term_check 0 "after_infer_fixate" (lift_check after_infer_fixate))
    1.57        |> prep_decl raw_supexpr init_class_body raw_elems;
    1.58      fun filter_element (Element.Fixes []) = NONE
    1.59        | filter_element (e as Element.Fixes _) = SOME e