# HG changeset patch # User wenzelm # Date 1737194940 -3600 # Node ID 5fd1dea4eb610411a419d721bce12d62ae01620c # Parent aa28d82d6b66264ab7fa7f010bb0cc5092d69e5b tuned; diff -r aa28d82d6b66 -r 5fd1dea4eb61 src/HOL/Import/import_data.ML --- a/src/HOL/Import/import_data.ML Sat Jan 18 11:03:18 2025 +0100 +++ b/src/HOL/Import/import_data.ML Sat Jan 18 11:09:00 2025 +0100 @@ -97,15 +97,15 @@ Theory.setup (Attrib.setup \<^binding>\import_const\ (Scan.lift Parse.name -- Scan.option (Scan.lift \<^keyword>\:\ |-- Args.const {proper = true, strict = false}) >> - (fn (s1, s2) => Thm.declaration_attribute - (fn th => Context.mapping (add_const_def s1 th s2) I))) + (fn (c, d) => Thm.declaration_attribute + (fn th => Context.mapping (add_const_def c th d) I))) "declare a theorem as an equality that maps the given constant") val _ = Theory.setup (Attrib.setup \<^binding>\import_type\ (Scan.lift (Parse.name -- Parse.name -- Parse.name) >> - (fn ((tyname, absname), repname) => Thm.declaration_attribute - (fn th => Context.mapping (add_typ_def tyname absname repname th) I))) + (fn ((c, abs), rep) => Thm.declaration_attribute + (fn th => Context.mapping (add_typ_def c abs rep th) I))) "declare a type_definition theorem as a map for an imported type with abs and rep") val _ = diff -r aa28d82d6b66 -r 5fd1dea4eb61 src/HOL/Import/import_rule.ML --- a/src/HOL/Import/import_rule.ML Sat Jan 18 11:03:18 2025 +0100 +++ b/src/HOL/Import/import_rule.ML Sat Jan 18 11:09:00 2025 +0100 @@ -210,8 +210,9 @@ fun tydef' tycname abs_name rep_name cP ct td_th thy = let val ctT = Thm.ctyp_of_cterm ct - val nonempty = Thm.instantiate' [SOME ctT] [SOME cP, SOME ct] - @{lemma "P t \ \x. x \ Collect P" by auto} + val nonempty = + Thm.instantiate' [SOME ctT] [SOME cP, SOME ct] + @{lemma "P t \ \x. x \ Collect P" by auto} val th2 = meta_mp nonempty td_th val c = (case Thm.concl_of th2 of