# HG changeset patch # User haftmann # Date 1401729701 -7200 # Node ID 6254c51cd2104295ff7996166511b9f446ee3c8a # Parent cf00d3c9db4331e971f15c5ccca81836cae0be63 formal treatment of dangling parameters for class abbrevs analogously to class consts diff -r cf00d3c9db43 -r 6254c51cd210 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Mon Jun 02 19:21:40 2014 +0200 +++ b/src/Pure/Isar/class.ML Mon Jun 02 19:21:41 2014 +0200 @@ -18,7 +18,7 @@ val init: class -> theory -> Proof.context val begin: class list -> sort -> Proof.context -> Proof.context val const: class -> (binding * mixfix) * term -> term list * term list -> local_theory -> local_theory - val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> term -> local_theory -> local_theory + val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> term -> term list * term list -> local_theory -> local_theory val redeclare_operations: theory -> sort -> Proof.context -> Proof.context val class_prefix: string -> string val register: class -> class list -> ((string * typ) * (string * typ)) list @@ -340,7 +340,7 @@ map fst (these_params (Proof_Context.theory_of lthy) [class]); val dangling_term_params = subtract (fn (v, Free (w, _)) => v = w | _ => false) class_param_names term_params; - in type_params @ dangling_term_params end; + in (type_params, dangling_term_params) end; fun global_def (b, eq) thy = thy @@ -367,19 +367,19 @@ |> Sign.add_const_constraint (c, SOME ty) end; -fun canonical_abbrev class phi prmode ((b, mx), rhs) thy = +fun canonical_abbrev class phi prmode dangling_term_params ((b, mx), rhs) thy = let val unchecks = these_unchecks thy [class]; - val b' = Morphism.binding phi b; val rhs' = Pattern.rewrite_term thy unchecks [] rhs; - val c' = Sign.full_name thy b'; - val ty' = Term.fastype_of rhs'; + val c' = Sign.full_name thy b; + val ty' = map Term.fastype_of dangling_term_params ---> Term.fastype_of rhs'; in thy - |> Sign.add_abbrev (#1 prmode) (b', Logic.varify_types_global rhs') + |> Sign.add_abbrev (#1 prmode) (b, Logic.varify_types_global (fold lambda dangling_term_params rhs')) |> snd |> Sign.notation true prmode [(Const (c', ty'), mx)] - |> not (#1 prmode = Print_Mode.input) ? register_operation class (c', (rhs', NONE)) + |> (null dangling_term_params andalso not (#1 prmode = Print_Mode.input)) + ? register_operation class (c', (rhs', NONE)) |> Sign.add_const_constraint (c', SOME ty') end; @@ -388,7 +388,7 @@ fun const class ((b, mx), lhs) params lthy = let val phi = morphism (Proof_Context.theory_of lthy) class; - val dangling_params = map (Morphism.term phi) (dangling_params_for lthy class params); + val dangling_params = map (Morphism.term phi) (uncurry append (dangling_params_for lthy class params)); in lthy |> class_const class Syntax.mode_default (b, lhs) @@ -399,14 +399,17 @@ |> synchronize_class_syntax_target class end; -fun abbrev class prmode ((b, mx), lhs) rhs' lthy = +fun abbrev class prmode ((b, mx), lhs) rhs' params lthy = let val phi = morphism (Proof_Context.theory_of lthy) class; + val dangling_term_params = map (Morphism.term phi) (snd (dangling_params_for lthy class params)); in lthy |> class_const class prmode (b, lhs) - |> Local_Theory.raw_theory (canonical_abbrev class phi prmode ((b, mx), rhs')) - |> Generic_Target.const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, NoSyn), lhs) + |> Local_Theory.raw_theory (canonical_abbrev class phi prmode dangling_term_params + ((Morphism.binding phi b, if null dangling_term_params then mx else NoSyn), rhs')) + |> Generic_Target.const (fn (this, other) => other <> 0 andalso this <> other) + prmode ((b, if null dangling_term_params then NoSyn else mx), lhs) |> synchronize_class_syntax_target class end; diff -r cf00d3c9db43 -r 6254c51cd210 src/Pure/Isar/named_target.ML --- a/src/Pure/Isar/named_target.ML Mon Jun 02 19:21:40 2014 +0200 +++ b/src/Pure/Isar/named_target.ML Mon Jun 02 19:21:41 2014 +0200 @@ -81,7 +81,7 @@ fun class_abbrev class prmode (b, mx) global_rhs params = Generic_Target.background_abbrev (b, global_rhs) (snd params) - #-> (fn (lhs, rhs) => Class.abbrev class prmode ((b, mx), lhs) rhs); + #-> (fn (lhs, rhs) => Class.abbrev class prmode ((b, mx), lhs) rhs params); fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) = if is_class then class_abbrev target