src/Pure/Isar/class_declaration.ML
changeset 46922 3717f3878714
parent 46856 28909eecdf5b
child 47311 1addbe2a7458
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Wed Mar 14 15:59:39 2012 +0100
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Wed Mar 14 17:52:38 2012 +0100
     1.3 @@ -198,10 +198,11 @@
     1.4  
     1.5  fun prep_class_spec prep_class prep_class_elems thy raw_supclasses raw_elems =
     1.6    let
     1.7 +    val thy_ctxt = Proof_Context.init_global thy;
     1.8  
     1.9      (* prepare import *)
    1.10      val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy));
    1.11 -    val sups = Sign.minimize_sort thy (map (prep_class thy) raw_supclasses);
    1.12 +    val sups = Sign.minimize_sort thy (map (prep_class thy_ctxt) raw_supclasses);
    1.13      val _ =
    1.14        (case filter_out (Class.is_class thy) sups of
    1.15          [] => ()
    1.16 @@ -219,7 +220,7 @@
    1.17      val sup_sort = inter_sort base_sort sups;
    1.18  
    1.19      (* process elements as class specification *)
    1.20 -    val class_ctxt = Class.begin sups base_sort (Proof_Context.init_global thy);
    1.21 +    val class_ctxt = Class.begin sups base_sort thy_ctxt;
    1.22      val ((_, _, syntax_elems), _) = class_ctxt
    1.23        |> Expression.cert_declaration supexpr I inferred_elems;
    1.24      fun check_vars e vs =
    1.25 @@ -243,7 +244,7 @@
    1.26    in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), (elems, global_syntax)) end;
    1.27  
    1.28  val cert_class_spec = prep_class_spec (K I) cert_class_elems;
    1.29 -val read_class_spec = prep_class_spec Sign.intern_class read_class_elems;
    1.30 +val read_class_spec = prep_class_spec Proof_Context.read_class read_class_elems;
    1.31  
    1.32  
    1.33  (* class establishment *)