# HG changeset patch # User haftmann # Date 1192192950 -7200 # Node ID c3d9cb3904715d05bb37c28204d59fa3a9394407 # Parent 7982fe02a50edbb893350df946fdead0cebdc1ec tuned diff -r 7982fe02a50e -r c3d9cb390471 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Fri Oct 12 14:42:29 2007 +0200 +++ b/src/Pure/Isar/class.ML Fri Oct 12 14:42:30 2007 +0200 @@ -14,22 +14,23 @@ -> theory -> class * theory val classrel_cmd: xstring * xstring -> theory -> Proof.state - val class: bool -> bstring -> class list -> Element.context_i Locale.element list + val class: bstring -> class list -> Element.context_i Locale.element list -> string list -> theory -> string * Proof.context - val class_cmd: bool -> bstring -> xstring list -> Element.context Locale.element list + val class_cmd: bstring -> xstring list -> Element.context Locale.element list -> xstring list -> theory -> string * Proof.context val init: class -> Proof.context -> Proof.context; val add_const_in_class: string -> (string * term) * Syntax.mixfix -> theory -> string * theory val add_abbrev_in_class: string -> Syntax.mode -> (string * term) * mixfix -> theory -> string * theory - val remove_constraint: sort -> string -> Proof.context -> Proof.context + val remove_constraint: class -> string -> Proof.context -> Proof.context + val class_of_locale: theory -> string -> class option + val locale_of_class: theory -> class -> string + val these_params: theory -> sort -> (string * (string * typ)) list val intro_classes_tac: thm list -> tactic val default_intro_classes_tac: thm list -> tactic - val class_of_locale: theory -> string -> class option - val locale_of_class: theory -> class -> string - val local_syntax: theory -> class -> bool val print_classes: theory -> unit + val uncheck: bool ref val instance_arity: (theory -> theory) -> arity list -> theory -> Proof.state val instance: arity list -> ((bstring * Attrib.src list) * term) list @@ -47,7 +48,6 @@ val unoverload_const: theory -> string * typ -> string val inst_const: theory -> string * string -> string val param_const: theory -> string -> (string * string) option - val params_of_sort: theory -> sort -> (string * (string * typ)) list end; structure Class : CLASS = @@ -63,8 +63,8 @@ val mx_local = if is_loc then mx else NoSyn; in (mx_global, mx_local) end; -fun prove_interpretation tac prfx_atts expr insts = - Locale.interpretation_i I prfx_atts expr insts +fun prove_interpretation tac prfx_atts expr inst = + Locale.interpretation_i I prfx_atts expr inst #> Proof.global_terminal_proof (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE) #> ProofContext.theory_of; @@ -323,32 +323,32 @@ inst: typ Symtab.table * term Symtab.table (*canonical interpretation*), intro: thm, - local_syntax: bool, defs: thm list, - operations: (string * (term * int) option) list, - (*constant name ~> (locale term, instantiaton index of class typ)*) - constraints: (string * typ) list + operations: (string * (term * (typ * int))) list + (*constant name ~> (locale term, (constant constraint, instantiaton index of class typ))*), + operations_rev: (string * string) list + (*locale operation ~> constant name*) }; fun rep_class_data (ClassData d) = d; -fun mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax), - (defs, (operations, constraints))) = +fun mk_class_data ((locale, consts, local_sort, inst, intro), + (defs, operations, operations_rev)) = ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst, - intro = intro, local_syntax = local_syntax, defs = defs, operations = operations, - constraints = constraints }; + intro = intro, defs = defs, operations = operations, + operations_rev = operations_rev }; fun map_class_data f (ClassData { locale, consts, local_sort, inst, intro, - local_syntax, defs, operations, constraints }) = - mk_class_data (f ((locale, consts, local_sort, inst, intro, local_syntax), - (defs, (operations, constraints)))); + defs, operations, operations_rev }) = + mk_class_data (f ((locale, consts, local_sort, inst, intro), + (defs, operations, operations_rev))); fun merge_class_data _ (ClassData { locale = locale, consts = consts, - local_sort = local_sort, inst = inst, intro = intro, local_syntax = local_syntax, - defs = defs1, operations = operations1, constraints = constraints1 }, - ClassData { locale = _, consts = _, local_sort = _, inst = _, intro = _, local_syntax = _, - defs = defs2, operations = operations2, constraints = constraints2 }) = - mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax), + local_sort = local_sort, inst = inst, intro = intro, + defs = defs1, operations = operations1, operations_rev = operations_rev1 }, + ClassData { locale = _, consts = _, local_sort = _, inst = _, intro = _, + defs = defs2, operations = operations2, operations_rev = operations_rev2 }) = + mk_class_data ((locale, consts, local_sort, inst, intro), (Thm.merge_thms (defs1, defs2), - (AList.merge (op =) (K true) (operations1, operations2), - AList.merge (op =) (K true) (constraints1, constraints2)))); + AList.merge (op =) (K true) (operations1, operations2), + AList.merge (op =) (K true) (operations_rev1, operations_rev2))); fun merge_pair f1 f2 ((x1, y1), (x2, y2)) = (f1 (x1, x2), f2 (y1, y2)); @@ -377,7 +377,7 @@ val ancestry = Graph.all_succs o fst o ClassData.get; -fun params_of_sort thy = +fun these_params thy = let fun params class = let @@ -397,10 +397,12 @@ fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy; -fun these_constraints thy = - maps (#constraints o the_class_data thy) o ancestry thy; +fun these_operations_rev thy = + maps (#operations_rev o the_class_data thy) o ancestry thy; -fun local_operation thy = Option.join oo AList.lookup (op =) o these_operations thy; +fun local_operation thy = AList.lookup (op =) o these_operations thy; + +fun global_operation thy = AList.lookup (op =) o these_operations_rev thy; fun sups_local_sort thy sort = let @@ -411,8 +413,6 @@ | [] => sort; in (sups, local_sort) end; -fun local_syntax thy = #local_syntax o the_class_data thy; - fun print_classes thy = let val ctxt = ProofContext.init thy; @@ -450,25 +450,24 @@ (* updaters *) -fun add_class_data ((class, superclasses), (locale, consts, local_sort, inst, intro, local_syntax)) = - ClassData.map (fn (gr, tab) => ( - gr - |> Graph.new_node (class, mk_class_data ((locale, (map o pairself) fst consts, - local_sort, inst, intro, local_syntax), - ([], (map (apfst fst o apsnd (SOME o rpair 0 o Free) o swap) consts, map snd consts)))) - |> fold (curry Graph.add_edge class) superclasses, - tab - |> Symtab.update (locale, class) - )); +fun add_class_data ((class, superclasses), (locale, cs, local_sort, inst, intro)) = + let + val operations = map (fn (v_ty, (c, ty)) => (c, (Free v_ty, (ty, 0)))) cs; + val cs = (map o pairself) fst cs; + val add_class = Graph.new_node (class, mk_class_data ((locale, + cs, local_sort, inst, intro), + ([], operations, []))) + #> fold (curry Graph.add_edge class) superclasses; + val add_locale = Symtab.update (locale, class); + in + ClassData.map (fn (gr, tab) => (add_class gr, add_locale tab)) + end; -fun register_const class (entry, def) = +fun register_operation class (entry, some_def) = (ClassData.map o apfst o Graph.map_node class o map_class_data o apsnd) - (fn (defs, (operations, constraints)) => - (def :: defs, (apsnd (SOME o snd) entry :: operations, apsnd fst entry :: constraints))); - -fun register_abbrev class (abbrev, ty) = - (ClassData.map o apfst o Graph.map_node class o map_class_data o apsnd o apsnd) - (fn (operations, constraints) => ((abbrev, NONE) :: operations, (abbrev, ty) :: constraints)); + (fn (defs, operations, operations_rev) => + (case some_def of NONE => defs | SOME def => def :: defs, + entry :: operations, (*FIXME*)operations_rev)); (** rule calculation, tactics and methods **) @@ -559,23 +558,30 @@ (** classes and class target **) -(* class context initialization *) +(* class context syntax *) -fun remove_constraint local_sort c ctxt = +fun internal_remove_constraint local_sort (c, (_, (ty, typidx))) ctxt = let - val ty = ProofContext.the_const_constraint ctxt c; - val ty' = map_atyps (fn ty as TFree (v, _) => if v = Name.aT - then TFree (v, local_sort) else ty | ty => ty) ty; + val consts = ProofContext.consts_of ctxt; + val typargs = Consts.typargs consts (c, ty); + val typargs' = nth_map typidx (K (TVar ((Name.aT, 0), local_sort))) typargs; + val ty' = Consts.instance consts (c, typargs'); + in ProofContext.add_const_constraint (c, SOME ty') ctxt end; + +fun remove_constraint class c ctxt = + let + val thy = ProofContext.theory_of ctxt; + val SOME entry = local_operation thy [class] c; in - ctxt - |> ProofContext.add_const_constraint (c, SOME ty') + internal_remove_constraint + ((#local_sort o the_class_data thy) class) (c, entry) ctxt end; fun sort_term_check sups local_sort ts ctxt = let val thy = ProofContext.theory_of ctxt; val local_operation = local_operation thy sups; - val constraints = these_constraints thy sups; + val constraints = these_operations thy sups |> (map o apsnd) (fst o snd); val consts = ProofContext.consts_of ctxt; fun check_typ (c, ty) (t', idx) = case nth (Consts.typargs consts (c, ty)) idx of TFree (v, _) => if v = Name.aT @@ -585,7 +591,7 @@ #> apsnd (insert (op =) vi) else I | _ => I; fun add_const (Const (c, ty)) = (case local_operation c - of SOME (t', idx) => check_typ (c, ty) (t', idx) + of SOME (t', (_, idx)) => check_typ (c, ty) (t', idx) | NONE => I) | add_const _ = I; val (cs, typarams) = (fold o fold_aterms) add_const ts ([], []); @@ -596,6 +602,23 @@ val ctxt' = fold (ProofContext.add_const_constraint o apsnd SOME) constraints ctxt; in (ts', ctxt') end; +val uncheck = ref false; + +fun sort_term_uncheck sups ts ctxt = + let + val thy = ProofContext.theory_of ctxt; + val global_param = AList.lookup (op =) (these_params thy sups) #> Option.map fst; + val global_operation = global_operation thy sups; + fun globalize (t as Free (v, ty)) = (case global_param v + of SOME c => Const (c, ty) + | NONE => t) + | globalize (t as Const (c, ty)) = (case global_operation c + of SOME c => Const (c, ty) + | NONE => t) + | globalize t = t; + val ts' = if ! uncheck then (map o map_aterms) globalize ts else ts; + in (ts', ctxt) end; + fun init_class_ctxt sups local_sort ctxt = let val operations = these_operations (ProofContext.theory_of ctxt) sups; @@ -603,9 +626,11 @@ ctxt |> Variable.declare_term (Logic.mk_type (TFree (Name.aT, local_sort))) - |> fold (remove_constraint local_sort o fst) operations + |> fold (internal_remove_constraint local_sort) operations |> Context.proof_map (Syntax.add_term_check 50 "class" - (sort_term_check sups local_sort)) + (sort_term_check sups local_sort) + #> Syntax.add_term_uncheck 50 "class" + (sort_term_uncheck sups)) end; fun init class ctxt = @@ -627,7 +652,7 @@ | Locale.Expr i => apsnd (cons (prep_expr thy i))) raw_includes_elems ([], []); val supexpr = Locale.Merge suplocales; val supparams = (map fst o Locale.parameters_of_expr thy) supexpr; - val supconsts = AList.make (the o AList.lookup (op =) (params_of_sort thy sups)) + val supconsts = AList.make (the o AList.lookup (op =) (these_params thy sups)) (map fst supparams); val mergeexpr = Locale.Merge (suplocales @ includes); val constrain = Element.Constrains ((map o apsnd o map_atyps) @@ -646,7 +671,6 @@ val read_class_spec = gen_class_spec Sign.intern_class Locale.intern_expr Locale.read_expr; val check_class_spec = gen_class_spec (K I) (K I) Locale.cert_expr; - fun define_class_params (name, raw_superclasses) raw_consts raw_dep_axioms other_consts thy = let val superclasses = map (Sign.certify_class thy) raw_superclasses; @@ -656,9 +680,8 @@ raw_dep_axioms thy cs |> (map o apsnd o map) (Sign.cert_prop thy) |> rpair thy; - fun add_constraint class (c, ty) = - Sign.add_const_constraint (c, SOME - (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty)); + fun constrain_typs class = (map o apsnd o Term.map_type_tfree) + (fn (v, _) => TFree (v, [class])) in thy |> Sign.add_path (Logic.const_of_class name) @@ -667,12 +690,13 @@ |-> (fn cs => mk_axioms cs #-> (fn axioms_prop => AxClass.define_class (name, superclasses) (map fst cs @ other_consts) axioms_prop - #-> (fn class => `(fn thy => AxClass.get_info thy class) - #-> (fn {axioms, ...} => fold (add_constraint class) cs - #> pair (class, (cs, axioms)))))) + #-> (fn class => `(fn _ => constrain_typs class cs) + #-> (fn cs' => `(fn thy => AxClass.get_info thy class) + #-> (fn {axioms, ...} => fold (Sign.add_const_constraint o apsnd SOME) cs' + #> pair (class, (cs', axioms))))))) end; -fun gen_class prep_spec prep_param local_syntax bname +fun gen_class prep_spec prep_param bname raw_supclasses raw_includes_elems raw_other_consts thy = let val (((sups, supconsts), (supsort, local_sort, mergeexpr)), elems) = @@ -729,7 +753,7 @@ add_class_data ((name_axclass, sups), (name_locale, map fst params ~~ consts, local_sort, (mk_instT name_axclass, mk_inst name_axclass (map fst globals) - (map snd supconsts @ consts)), class_intro, local_syntax)) + (map snd supconsts @ consts)), class_intro)) #> note_intro name_axclass class_intro #> class_interpretation name_axclass axioms [] #> pair name_axclass @@ -748,8 +772,8 @@ fun export_fixes thy class = let - val consts = params_of_sort thy [class]; - fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) consts v + val cs = these_params thy [class]; + fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) cs v of SOME (c, _) => Const (c, ty) | NONE => t) | subst_aterm t = t; @@ -757,10 +781,10 @@ fun mk_operation_entry thy (c, rhs) = let - val ty = fastype_of rhs; + val ty = Logic.unvarifyT (Sign.the_const_constraint thy c); val typargs = Sign.const_typargs thy (c, ty); val typidx = find_index (fn TFree (w, _) => Name.aT = w | _ => false) typargs; - in (c, (ty, (rhs, typidx))) end; + in (c, (rhs, (ty, typidx))) end; fun add_const_in_class class ((c, rhs), syn) thy = let @@ -771,10 +795,9 @@ val n2 = NameSpace.qualifier n1; val n3 = NameSpace.base n1; in NameSpace.implode [n2, prfx, n3] end; - val constrain_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) [class]; val rhs' = export_fixes thy class rhs; val subst_typ = Term.map_type_tfree (fn var as (w, sort) => - if w = Name.aT then TFree (w, constrain_sort sort) else TFree var); + if w = Name.aT then TFree (w, [class]) else TFree var); val ty' = Term.fastype_of rhs'; val ty'' = subst_typ ty'; val c' = mk_name c; @@ -783,12 +806,13 @@ fun interpret def thy = let val def' = symmetric def; - val def_eq = Thm.prop_of def'; - val entry = mk_operation_entry thy (c', rhs); + val def_eq = (map_types Logic.unvarifyT o Thm.prop_of) def'; in thy |> class_interpretation class [def'] [def_eq] - |> register_const class (entry, def') + |> Sign.add_const_constraint (c', SOME ty'') + |> `(fn thy => mk_operation_entry thy (c', rhs)) + |-> (fn entry => register_operation class (entry, SOME def')) end; in thy @@ -798,7 +822,6 @@ |> Sign.sticky_prefix prfx |> PureThy.add_defs_i false [(def, [])] |-> (fn [def] => interpret def) - |> Sign.add_const_constraint (c', SOME ty'') |> Sign.restore_naming thy |> pair c' end; @@ -818,10 +841,11 @@ val c' = mk_name c; val rhs' = export_fixes thy class rhs; val ty' = fastype_of rhs'; + val entry = mk_operation_entry thy (c', rhs); in thy |> Sign.notation true prmode [(Const (c', ty'), syn)] - |> register_abbrev class (c', ty') + |> register_operation class (entry, NONE) |> pair c' end; diff -r 7982fe02a50e -r c3d9cb390471 src/Pure/Isar/instance.ML --- a/src/Pure/Isar/instance.ML Fri Oct 12 14:42:29 2007 +0200 +++ b/src/Pure/Isar/instance.ML Fri Oct 12 14:42:30 2007 +0200 @@ -38,7 +38,7 @@ ((param ^ "_" ^ NameSpace.base tyco, map_atyps (K ty_subst) ty), Class.unoverload_const thy (c, ty)); fun get_params ((tyco, vs), sort) = - Class.params_of_sort thy sort + Class.these_params thy sort |> map (get_param tyco (Type (tyco, map TFree vs))); val params = maps get_params arities; val ctxt = diff -r 7982fe02a50e -r c3d9cb390471 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Fri Oct 12 14:42:29 2007 +0200 +++ b/src/Pure/Isar/locale.ML Fri Oct 12 14:42:30 2007 +0200 @@ -2104,7 +2104,7 @@ (* infer types *) val res = Syntax.check_terms ctxt (map Logic.mk_type type_parms @ - map (uncurry TypeInfer.constrain) (given_parm_types ~~ given_insts') @ + map2 TypeInfer.constrain given_parm_types given_insts' @ eqns'); val ctxt' = ctxt |> fold Variable.auto_fixes res; diff -r 7982fe02a50e -r c3d9cb390471 src/Pure/Isar/subclass.ML --- a/src/Pure/Isar/subclass.ML Fri Oct 12 14:42:29 2007 +0200 +++ b/src/Pure/Isar/subclass.ML Fri Oct 12 14:42:30 2007 +0200 @@ -2,14 +2,14 @@ ID: $Id$ Author: Florian Haftmann, TU Muenchen -Prove subclass relations between type classes +Prove subclass relationship between type classes. *) signature SUBCLASS = sig val subclass: class -> local_theory -> Proof.state val subclass_cmd: xstring -> local_theory -> Proof.state - (*FIXME val prove_subclass: tactic -> class * class -> theory -> theory*) + val prove_subclass: tactic -> class -> local_theory -> local_theory end; structure Subclass : SUBCLASS = @@ -48,71 +48,82 @@ local -fun mk_subclass_rule lthy sup = +fun gen_subclass prep_class do_proof raw_sup lthy = let - (*FIXME check for proper parameter inclusion (consts_of) (?)*) - val ctxt = LocalTheory.target_of lthy; - val thy = ProofContext.theory_of ctxt; - val locale = Class.locale_of_class thy sup; - in - Locale.global_asms_of thy locale - |> maps snd - |> map (ObjectLogic.ensure_propT thy) - end; - -fun gen_subclass prep_class raw_sup lthy = - let - (*FIXME cleanup, provide tactical interface*) val ctxt = LocalTheory.target_of lthy; val thy = ProofContext.theory_of ctxt; val ctxt_thy = ProofContext.init thy; val sup = prep_class thy raw_sup; - val sub = case Option.mapPartial (Class.class_of_locale thy) - (TheoryTarget.peek lthy) + val sub = case Option.mapPartial (Class.class_of_locale thy) (TheoryTarget.peek lthy) of NONE => error "not in class context" | SOME sub => sub; - val export = - Assumption.export false ctxt ctxt_thy - #> singleton (Variable.export ctxt ctxt_thy); + val sub_params = map fst (Class.these_params thy [sub]); + val sup_params = map fst (Class.these_params thy [sup]); + val err_params = subtract (op =) sub_params sup_params; + val _ = if null err_params then [] else + error ("Class " ^ Sign.string_of_sort thy [sub] ^ " lacks parameter(s) " ^ + commas_quote err_params ^ " of " ^ Sign.string_of_sort thy [sup]); + val sublocale_prop = + Locale.global_asms_of thy (Class.locale_of_class thy sup) + |> maps snd + |> map (ObjectLogic.ensure_propT thy); + val supclasses = Sign.complete_sort thy [sup] + |> filter_out (fn class => Sign.subsort thy ([sub], [class])); + val supclasses' = remove (op =) sup supclasses; + val _ = if null supclasses' then () else + error ("The following superclasses of " ^ sup + ^ " are no superclass of " ^ sub ^ ": " + ^ commas supclasses'); + (*FIXME*) + val sub_ax = #axioms (AxClass.get_info thy sub); + val sub_inst = Thm.ctyp_of thy (TVar ((Name.aT, 0), [sub])); val loc_name = Class.locale_of_class thy sub; val loc_expr = Locale.Locale (Class.locale_of_class thy sup); - fun prove_classrel interp thy = + fun prove_classrel subclass_rule = let - val classes = Sign.complete_sort thy [sup] - |> filter_out (fn class' => Sign.subsort thy ([sub], [class'])); - fun instance_subclass (class1, class2) thy = + fun add_classrel sup' thy = let - val ax = #axioms (AxClass.get_info thy class1); - val intro = #intro (AxClass.get_info thy class2) - |> Drule.instantiate' [SOME (Thm.ctyp_of thy - (TVar ((Name.aT, 0), [class1])))] []; - val thm = - intro - |> OF_LAST (interp OF ax) - |> strip_all_ofclass thy (Sign.super_classes thy class2); + val classrel = + #intro (AxClass.get_info thy sup') + |> Drule.instantiate' [SOME sub_inst] [] + |> OF_LAST (subclass_rule OF sub_ax) + |> strip_all_ofclass thy (Sign.super_classes thy sup'); in - thy |> AxClass.add_classrel thm + AxClass.add_classrel classrel thy end; in - thy |> fold_rev (curry instance_subclass sub) classes + fold_rev add_classrel supclasses end; - fun after_qed [thms] = + fun prove_interpretation sublocale_rule = + prove_interpretation_in (ProofContext.fact_tac [sublocale_rule] 1) + I (loc_name, loc_expr) + fun after_qed thms = let - val thm = Conjunction.intr_balanced thms; - val interp = export thm; + val sublocale_rule = Conjunction.intr_balanced thms; + val subclass_rule = sublocale_rule + |> Assumption.export false ctxt ctxt_thy + |> singleton (Variable.export ctxt ctxt_thy); in - LocalTheory.theory (prove_classrel interp - #> prove_interpretation_in (ProofContext.fact_tac [thm] 1) - I (loc_name, loc_expr)) + LocalTheory.theory (prove_classrel subclass_rule + #> prove_interpretation sublocale_rule) (*#> (fn lthy => LocalTheory.reinit lthy thy) FIXME does not work as expected*) end; + in + do_proof after_qed sublocale_prop lthy + end; - in Proof.theorem_i NONE after_qed [map (rpair []) (mk_subclass_rule lthy sup)] lthy end; +fun user_proof after_qed props = + Proof.theorem_i NONE (after_qed o the_single) [map (rpair []) props]; + +fun tactic_proof tac after_qed props lthy = + after_qed (Goal.prove_multi (LocalTheory.target_of lthy) [] [] props + (K tac)) lthy; in -val subclass = gen_subclass (K I); -val subclass_cmd = gen_subclass Sign.read_class; +val subclass = gen_subclass (K I) user_proof; +val subclass_cmd = gen_subclass Sign.read_class user_proof; +fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac); end; (*local*) diff -r 7982fe02a50e -r c3d9cb390471 src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Fri Oct 12 14:42:29 2007 +0200 +++ b/src/Pure/Isar/theory_target.ML Fri Oct 12 14:42:30 2007 +0200 @@ -203,7 +203,7 @@ in (((c, mx2), t), thy') end; fun const_class (SOME class) ((c, _), mx) (_, t) = LocalTheory.raw_theory_result (Class.add_const_in_class class ((c, t), mx)) - #-> Class.remove_constraint [class] + #-> Class.remove_constraint class | const_class NONE _ _ = I; fun hide_abbrev (SOME class) abbrs thy = let @@ -274,7 +274,7 @@ val mx3 = if is_loc then NoSyn else mx1; fun add_abbrev_in_class (SOME class) abbr = LocalTheory.raw_theory_result (Class.add_abbrev_in_class class prmode abbr) - #-> (fn c => Class.remove_constraint [class] c) + #-> Class.remove_constraint class | add_abbrev_in_class NONE _ = I; in lthy