src/Pure/Isar/local_theory.ML
changeset 35798 fd1bb29f8170
parent 35738 98fd035c3fe3
child 36004 5d79ca55a52b
     1.1 --- a/src/Pure/Isar/local_theory.ML	Mon Mar 15 15:13:22 2010 +0100
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Mon Mar 15 18:59:16 2010 +0100
     1.3 @@ -39,9 +39,8 @@
     1.4      local_theory -> (string * thm list) list * local_theory
     1.5    val notes_kind: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
     1.6      local_theory -> (string * thm list) list * local_theory
     1.7 -  val type_syntax: bool -> declaration -> local_theory -> local_theory
     1.8 -  val term_syntax: bool -> declaration -> local_theory -> local_theory
     1.9    val declaration: bool -> declaration -> local_theory -> local_theory
    1.10 +  val syntax_declaration: bool -> declaration -> local_theory -> local_theory
    1.11    val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
    1.12    val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
    1.13    val class_alias: binding -> class -> local_theory -> local_theory
    1.14 @@ -72,9 +71,8 @@
    1.15    notes: string ->
    1.16      (Attrib.binding * (thm list * Attrib.src list) list) list ->
    1.17      local_theory -> (string * thm list) list * local_theory,
    1.18 -  type_syntax: bool -> declaration -> local_theory -> local_theory,
    1.19 -  term_syntax: bool -> declaration -> local_theory -> local_theory,
    1.20    declaration: bool -> declaration -> local_theory -> local_theory,
    1.21 +  syntax_declaration: bool -> declaration -> local_theory -> local_theory,
    1.22    reinit: local_theory -> local_theory,
    1.23    exit: local_theory -> Proof.context};
    1.24  
    1.25 @@ -195,9 +193,8 @@
    1.26  val abbrev = apsnd checkpoint ooo operation2 #abbrev;
    1.27  val define = apsnd checkpoint oo operation1 #define;
    1.28  val notes_kind = apsnd checkpoint ooo operation2 #notes;
    1.29 -val type_syntax = checkpoint ooo operation2 #type_syntax;
    1.30 -val term_syntax = checkpoint ooo operation2 #term_syntax;
    1.31  val declaration = checkpoint ooo operation2 #declaration;
    1.32 +val syntax_declaration = checkpoint ooo operation2 #syntax_declaration;
    1.33  
    1.34  val notes = notes_kind "";
    1.35  fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
    1.36 @@ -207,24 +204,24 @@
    1.37  
    1.38  fun type_notation add mode raw_args lthy =
    1.39    let val args = map (apfst (Morphism.typ (target_morphism lthy))) raw_args
    1.40 -  in type_syntax false (ProofContext.target_type_notation add mode args) lthy end;
    1.41 +  in syntax_declaration false (ProofContext.target_type_notation add mode args) lthy end;
    1.42  
    1.43  fun notation add mode raw_args lthy =
    1.44    let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
    1.45 -  in term_syntax false (ProofContext.target_notation add mode args) lthy end;
    1.46 +  in syntax_declaration false (ProofContext.target_notation add mode args) lthy end;
    1.47  
    1.48  
    1.49  (* name space aliases *)
    1.50  
    1.51 -fun alias syntax_declaration global_alias local_alias b name =
    1.52 +fun alias global_alias local_alias b name =
    1.53    syntax_declaration false (fn phi =>
    1.54      let val b' = Morphism.binding phi b
    1.55      in Context.mapping (global_alias b' name) (local_alias b' name) end)
    1.56    #> local_alias b name;
    1.57  
    1.58 -val class_alias = alias type_syntax Sign.class_alias ProofContext.class_alias;
    1.59 -val type_alias = alias type_syntax Sign.type_alias ProofContext.type_alias;
    1.60 -val const_alias = alias term_syntax Sign.const_alias ProofContext.const_alias;
    1.61 +val class_alias = alias Sign.class_alias ProofContext.class_alias;
    1.62 +val type_alias = alias Sign.type_alias ProofContext.type_alias;
    1.63 +val const_alias = alias Sign.const_alias ProofContext.const_alias;
    1.64  
    1.65  
    1.66  (* init *)