src/Pure/Isar/class.ML
changeset 38619 25e401d53900
parent 38392 8a3ca8b96b23
child 38756 d07959fabde6
     1.1 --- a/src/Pure/Isar/class.ML	Thu Aug 19 18:44:26 2010 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Fri Aug 20 08:52:01 2010 +0200
     1.3 @@ -17,9 +17,8 @@
     1.4    val print_classes: theory -> unit
     1.5    val init: class -> theory -> Proof.context
     1.6    val begin: class list -> sort -> Proof.context -> Proof.context
     1.7 -  val const: class -> (binding * mixfix) * (term list * term) -> theory -> theory
     1.8 -  val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> theory -> theory
     1.9 -  val refresh_syntax: class -> Proof.context -> Proof.context
    1.10 +  val const: class -> (binding * mixfix) * (term list * term) -> local_theory -> local_theory
    1.11 +  val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory
    1.12    val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
    1.13    val class_prefix: string -> string
    1.14    val register: class -> class list -> ((string * typ) * (string * typ)) list
    1.15 @@ -286,12 +285,6 @@
    1.16      |> Overloading.set_primary_constraints
    1.17    end;
    1.18  
    1.19 -fun refresh_syntax class ctxt =
    1.20 -  let
    1.21 -    val thy = ProofContext.theory_of ctxt;
    1.22 -    val base_sort = base_sort thy class;
    1.23 -  in synchronize_class_syntax [class] base_sort ctxt end;
    1.24 -
    1.25  fun redeclare_operations thy sort =
    1.26    fold (redeclare_const thy o fst) (these_operations thy sort);
    1.27  
    1.28 @@ -312,7 +305,15 @@
    1.29  
    1.30  val class_prefix = Logic.const_of_class o Long_Name.base_name;
    1.31  
    1.32 -fun const class ((c, mx), (type_params, dict)) thy =
    1.33 +fun target_extension f class lthy =
    1.34 +  lthy
    1.35 +  |> Local_Theory.raw_theory f
    1.36 +  |> Local_Theory.target (synchronize_class_syntax [class]
    1.37 +      (base_sort (ProofContext.theory_of lthy) class));
    1.38 +
    1.39 +local
    1.40 +
    1.41 +fun target_const class ((c, mx), (type_params, dict)) thy =
    1.42    let
    1.43      val morph = morphism thy class;
    1.44      val b = Morphism.binding morph c;
    1.45 @@ -334,7 +335,7 @@
    1.46      |> Sign.add_const_constraint (c', SOME ty')
    1.47    end;
    1.48  
    1.49 -fun abbrev class prmode ((c, mx), rhs) thy =
    1.50 +fun target_abbrev class prmode ((c, mx), rhs) thy =
    1.51    let
    1.52      val morph = morphism thy class;
    1.53      val unchecks = these_unchecks thy [class];
    1.54 @@ -352,6 +353,13 @@
    1.55      |> not (#1 prmode = Print_Mode.input) ? register_operation class (c', (rhs', NONE))
    1.56    end;
    1.57  
    1.58 +in
    1.59 +
    1.60 +fun const class arg = target_extension (target_const class arg) class;
    1.61 +fun abbrev class prmode arg = target_extension (target_abbrev class prmode arg) class;
    1.62 +
    1.63 +end;
    1.64 +
    1.65  
    1.66  (* simple subclasses *)
    1.67