src/Pure/Isar/class_target.ML
changeset 30344 10a67c5ddddb
parent 30280 eb98b49ef835
child 30364 577edc39b501
     1.1 --- a/src/Pure/Isar/class_target.ML	Sat Mar 07 22:12:07 2009 +0100
     1.2 +++ b/src/Pure/Isar/class_target.ML	Sat Mar 07 22:16:50 2009 +0100
     1.3 @@ -24,9 +24,9 @@
     1.4    val begin: class list -> sort -> Proof.context -> Proof.context
     1.5    val init: class -> theory -> Proof.context
     1.6    val declare: class -> Properties.T
     1.7 -    -> (string * mixfix) * term -> theory -> theory
     1.8 +    -> (binding * mixfix) * term -> theory -> theory
     1.9    val abbrev: class -> Syntax.mode -> Properties.T
    1.10 -    -> (string * mixfix) * term -> theory -> theory
    1.11 +    -> (binding * mixfix) * term -> theory -> theory
    1.12    val class_prefix: string -> string
    1.13    val refresh_syntax: class -> Proof.context -> Proof.context
    1.14    val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
    1.15 @@ -52,12 +52,12 @@
    1.16    val default_intro_tac: Proof.context -> thm list -> tactic
    1.17  
    1.18    (*old axclass layer*)
    1.19 -  val axclass_cmd: bstring * xstring list
    1.20 +  val axclass_cmd: binding * xstring list
    1.21      -> (Attrib.binding * string list) list
    1.22      -> theory -> class * theory
    1.23    val classrel_cmd: xstring * xstring -> theory -> Proof.state
    1.24    val instance_arity: (theory -> theory) -> arity -> theory -> Proof.state
    1.25 -  val instance_arity_cmd: bstring * xstring list * xstring -> theory -> Proof.state
    1.26 +  val instance_arity_cmd: xstring * xstring list * xstring -> theory -> Proof.state
    1.27  end;
    1.28  
    1.29  structure Class_Target : CLASS_TARGET =
    1.30 @@ -363,8 +363,8 @@
    1.31  fun declare class pos ((c, mx), dict) thy =
    1.32    let
    1.33      val morph = morphism thy class;
    1.34 -    val b = Morphism.binding morph (Binding.name c);
    1.35 -    val b_def = Morphism.binding morph (Binding.name (c ^ "_dict"));
    1.36 +    val b = Morphism.binding morph c;
    1.37 +    val b_def = Morphism.binding morph (Binding.suffix_name "_dict" b);
    1.38      val c' = Sign.full_name thy b;
    1.39      val dict' = Morphism.term morph dict;
    1.40      val ty' = Term.fastype_of dict';
    1.41 @@ -386,7 +386,7 @@
    1.42    let
    1.43      val morph = morphism thy class;
    1.44      val unchecks = these_unchecks thy [class];
    1.45 -    val b = Morphism.binding morph (Binding.name c);
    1.46 +    val b = Morphism.binding morph c;
    1.47      val c' = Sign.full_name thy b;
    1.48      val rhs' = Pattern.rewrite_term thy unchecks [] rhs;
    1.49      val ty' = Term.fastype_of rhs';