src/Pure/Isar/class_declaration.ML
changeset 47311 1addbe2a7458
parent 46922 3717f3878714
child 51551 88d1d19fb74f
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Tue Apr 03 17:48:16 2012 +0200
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Tue Apr 03 18:22:14 2012 +0200
     1.3 @@ -157,7 +157,7 @@
     1.4        fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
     1.5        #> Class.redeclare_operations thy sups
     1.6        #> Context.proof_map (Syntax_Phases.term_check 0 "singleton_fixate" (K singleton_fixate));
     1.7 -    val ((raw_supparams, _, raw_inferred_elems), _) =
     1.8 +    val ((raw_supparams, _, raw_inferred_elems, _), _) =
     1.9        Proof_Context.init_global thy
    1.10        |> Context.proof_map (Syntax_Phases.term_check 0 "after_infer_fixate" (K after_infer_fixate))
    1.11        |> prep_decl raw_supexpr init_class_body raw_elems;
    1.12 @@ -221,7 +221,7 @@
    1.13  
    1.14      (* process elements as class specification *)
    1.15      val class_ctxt = Class.begin sups base_sort thy_ctxt;
    1.16 -    val ((_, _, syntax_elems), _) = class_ctxt
    1.17 +    val ((_, _, syntax_elems, _), _) = class_ctxt
    1.18        |> Expression.cert_declaration supexpr I inferred_elems;
    1.19      fun check_vars e vs =
    1.20        if null vs then