src/Pure/Isar/class.ML
changeset 25060 17c313217998
parent 25038 522abf8a5f87
child 25062 af5ef0d4d655
     1.1 --- a/src/Pure/Isar/class.ML	Tue Oct 16 19:45:56 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Tue Oct 16 19:45:57 2007 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4      -> string list -> theory -> string * Proof.context
     1.5    val class_cmd: bstring -> xstring list -> Element.context Locale.element list
     1.6      -> xstring list -> theory -> string * Proof.context
     1.7 -  val init: class -> Proof.context -> Proof.context;
     1.8 +  val init: class -> Proof.context -> Proof.context
     1.9    val add_const_in_class: string -> (string * mixfix) * (string * term)
    1.10      -> theory -> string * theory
    1.11    val add_abbrev_in_class: string -> Syntax.mode -> (string * mixfix) * (string * term)
    1.12 @@ -588,7 +588,7 @@
    1.13        #> (map_types o map_type_tvar) (fn var as (vi, _) => if member (op =) typarams vi
    1.14             then TFree (Name.aT, local_sort) else TVar var)) ts;
    1.15      val ctxt' = fold (ProofContext.add_const_constraint o apsnd SOME) constraints ctxt;
    1.16 -  in (ts', ctxt') end;
    1.17 +  in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt') end;
    1.18  
    1.19  val uncheck = ref false;
    1.20  
    1.21 @@ -605,7 +605,7 @@
    1.22            | NONE => t)
    1.23        | globalize t = t;
    1.24      val ts' = if ! uncheck then (map o map_aterms) globalize ts else ts;
    1.25 -  in (ts', ctxt) end;
    1.26 +  in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end;
    1.27  
    1.28  fun init_class_ctxt sups local_sort ctxt =
    1.29    let