src/Pure/Isar/class.ML
changeset 25311 aa750e3a581c
parent 25268 58146cb7bf44
child 25318 c8352b38d47d
     1.1 --- a/src/Pure/Isar/class.ML	Tue Nov 06 13:12:52 2007 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Tue Nov 06 13:12:53 2007 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4      -> xstring list -> theory -> string * Proof.context
     1.5    val is_class: theory -> class -> bool
     1.6    val these_params: theory -> sort -> (string * (string * typ)) list
     1.7 -  val init: class -> Proof.context -> Proof.context
     1.8 +  val init: class -> theory -> Proof.context
     1.9    val add_logical_const: string -> Markup.property list
    1.10      -> (string * mixfix) * term -> theory -> theory
    1.11    val add_syntactic_const: string -> Syntax.mode -> Markup.property list
    1.12 @@ -716,12 +716,10 @@
    1.13        Syntax.add_term_check 0 "class" sort_term_check
    1.14        #> Syntax.add_term_uncheck 0 "class" sort_term_uncheck)
    1.15  
    1.16 -fun init class ctxt =
    1.17 -  let
    1.18 -    val thy = ProofContext.theory_of ctxt;
    1.19 -  in
    1.20 -    init_ctxt thy [class] ((#base_sort o the_class_data thy) class) ctxt
    1.21 -  end;
    1.22 +fun init class thy =
    1.23 +  thy
    1.24 +  |> Locale.init class
    1.25 +  |> init_ctxt thy [class] ((#base_sort o the_class_data thy) class);
    1.26  
    1.27  
    1.28  (* class definition *)
    1.29 @@ -827,8 +825,9 @@
    1.30      thy
    1.31      |> Locale.add_locale_i (SOME "") bname mergeexpr elems
    1.32      |> snd
    1.33 -    |> ProofContext.theory (`extract_params
    1.34 -      #-> (fn (all_params, params) =>
    1.35 +    |> ProofContext.theory_of
    1.36 +    |> `extract_params
    1.37 +    |-> (fn (all_params, params) =>
    1.38          define_class_params (bname, supsort) params
    1.39            (extract_assumes params) other_consts
    1.40        #-> (fn (_, (consts, axioms)) =>
    1.41 @@ -842,7 +841,7 @@
    1.42              mk_inst class (map snd supconsts @ consts),
    1.43                calculate_morphism class (supconsts @ (map (fst o fst) params ~~ consts)), class_intro))
    1.44        #> class_interpretation class axioms []
    1.45 -      )))))
    1.46 +      ))))
    1.47      |> init class
    1.48      |> pair class
    1.49    end;