src/Pure/Isar/class_declaration.ML
changeset 42402 c7139609b67d
parent 42375 774df7c59508
child 42494 eef1a23c9077
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Tue Apr 19 10:50:54 2011 +0200
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Tue Apr 19 14:57:09 2011 +0200
     1.3 @@ -139,19 +139,18 @@
     1.4            (fn T as TFree _ => T | T as TVar (vi, _) =>
     1.5              if Type_Infer.is_param vi then Type_Infer.param 0 (Name.aT, sort') else T) Ts
     1.6        end;
     1.7 -    fun add_typ_check level name f = Context.proof_map
     1.8 -      (Syntax.add_typ_check level name (fn Ts => fn ctxt =>
     1.9 -        let val Ts' = f Ts in if eq_list (op =) (Ts, Ts') then NONE else SOME (Ts', ctxt) end));
    1.10  
    1.11      (* preprocessing elements, retrieving base sort from type-checked elements *)
    1.12 -    val raw_supexpr = (map (fn sup => (sup, (("", false),
    1.13 -      Expression.Positional []))) sups, []);
    1.14 -    val init_class_body = fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
    1.15 +    val raw_supexpr =
    1.16 +      (map (fn sup => (sup, (("", false), Expression.Positional []))) sups, []);
    1.17 +    val init_class_body =
    1.18 +      fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
    1.19        #> Class.redeclare_operations thy sups
    1.20 -      #> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc
    1.21 -      #> add_typ_check ~10 "singleton_fixate" singleton_fixate;
    1.22 -    val ((raw_supparams, _, raw_inferred_elems), _) = Proof_Context.init_global thy
    1.23 -      |> add_typ_check 5 "after_infer_fixate" after_infer_fixate
    1.24 +      #> Context.proof_map (Syntax.add_typ_check 10 "reject_bcd_etc" (K reject_bcd_etc))
    1.25 +      #> Context.proof_map (Syntax.add_typ_check ~10 "singleton_fixate" (K singleton_fixate));
    1.26 +    val ((raw_supparams, _, raw_inferred_elems), _) =
    1.27 +      Proof_Context.init_global thy
    1.28 +      |> Context.proof_map (Syntax.add_typ_check 5 "after_infer_fixate" (K after_infer_fixate))
    1.29        |> prep_decl raw_supexpr init_class_body raw_elems;
    1.30      fun filter_element (Element.Fixes []) = NONE
    1.31        | filter_element (e as Element.Fixes _) = SOME e
    1.32 @@ -165,7 +164,7 @@
    1.33      fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs
    1.34        | fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs
    1.35        | fold_element_types f (Element.Assumes assms) = fold (fold (fn (t, ts) =>
    1.36 -          fold_types f t #> (fold o fold_types) f ts) o snd) assms
    1.37 +          fold_types f t #> (fold o fold_types) f ts) o snd) assms;
    1.38      val base_sort = if null inferred_elems then proto_base_sort else
    1.39        case (fold o fold_element_types) Term.add_tfreesT inferred_elems []
    1.40         of [] => error "No type variable in class specification"