src/Pure/Isar/class_declaration.ML
changeset 38435 1e1ef69ec0de
parent 38390 cb72d89bb444
child 38493 95a41e6ef5a8
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Fri Aug 13 14:45:07 2010 +0200
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Fri Aug 13 17:17:04 2010 +0200
     1.3 @@ -130,8 +130,8 @@
     1.4              | _ => error "Multiple type variables in class specification.";
     1.5        in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end;
     1.6      fun add_typ_check level name f = Context.proof_map
     1.7 -      (Syntax.add_typ_check level name (fn xs => fn ctxt =>
     1.8 -        let val xs' = f xs in if eq_list (op =) (xs, xs') then NONE else SOME (xs', ctxt) end));
     1.9 +      (Syntax.add_typ_check level name (fn Ts => fn ctxt =>
    1.10 +        let val Ts' = f Ts in if eq_list (op =) (Ts, Ts') then NONE else SOME (Ts', ctxt) end));
    1.11  
    1.12      (* preprocessing elements, retrieving base sort from type-checked elements *)
    1.13      val init_class_body = fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints
    1.14 @@ -140,16 +140,21 @@
    1.15        #> add_typ_check ~10 "singleton_fixate" singleton_fixate;
    1.16      val raw_supexpr = (map (fn sup => (sup, (("", false),
    1.17        Expression.Positional []))) sups, []);
    1.18 -    val ((raw_supparams, _, inferred_elems), _) = ProofContext.init_global thy
    1.19 +    val ((raw_supparams, _, raw_inferred_elems), _) = ProofContext.init_global thy
    1.20        |> prep_decl raw_supexpr init_class_body raw_elems;
    1.21 +    fun filter_element (Element.Fixes []) = NONE
    1.22 +      | filter_element (e as Element.Fixes _) = SOME e
    1.23 +      | filter_element (Element.Constrains []) = NONE
    1.24 +      | filter_element (e as Element.Constrains _) = SOME e
    1.25 +      | filter_element (Element.Assumes []) = NONE
    1.26 +      | filter_element (e as Element.Assumes _) = SOME e
    1.27 +      | filter_element (Element.Defines _) = error ("\"defines\" element not allowed in class specification.")
    1.28 +      | filter_element (Element.Notes _) = error ("\"notes\" element not allowed in class specification.");
    1.29 +    val inferred_elems = map_filter filter_element raw_inferred_elems;
    1.30      fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs
    1.31        | fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs
    1.32        | fold_element_types f (Element.Assumes assms) = fold (fold (fn (t, ts) =>
    1.33            fold_types f t #> (fold o fold_types) f ts) o snd) assms
    1.34 -      | fold_element_types f (Element.Defines _) =
    1.35 -          error ("\"defines\" element not allowed in class specification.")
    1.36 -      | fold_element_types f (Element.Notes _) =
    1.37 -          error ("\"notes\" element not allowed in class specification.");
    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"