src/Pure/Isar/class_declaration.ML
changeset 45429 fd58cbf8cae3
parent 45421 2bef6da4a6a6
child 45431 924c2f6dcd05
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Wed Nov 09 19:01:50 2011 +0100
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Wed Nov 09 20:47:11 2011 +0100
     1.3 @@ -147,11 +147,11 @@
     1.4      val init_class_body =
     1.5        fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
     1.6        #> Class.redeclare_operations thy sups
     1.7 -      #> Context.proof_map (Syntax.add_typ_check 10 "reject_bcd_etc" (K reject_bcd_etc))
     1.8 -      #> Context.proof_map (Syntax.add_typ_check ~10 "singleton_fixate" (K singleton_fixate));
     1.9 +      #> Context.proof_map (Syntax_Phases.typ_check 10 "reject_bcd_etc" (K reject_bcd_etc))
    1.10 +      #> Context.proof_map (Syntax_Phases.typ_check ~10 "singleton_fixate" (K singleton_fixate));
    1.11      val ((raw_supparams, _, raw_inferred_elems), _) =
    1.12        Proof_Context.init_global thy
    1.13 -      |> Context.proof_map (Syntax.add_typ_check 5 "after_infer_fixate" (K after_infer_fixate))
    1.14 +      |> Context.proof_map (Syntax_Phases.typ_check 5 "after_infer_fixate" (K after_infer_fixate))
    1.15        |> prep_decl raw_supexpr init_class_body raw_elems;
    1.16      fun filter_element (Element.Fixes []) = NONE
    1.17        | filter_element (e as Element.Fixes _) = SOME e