# HG changeset patch # User wenzelm # Date 1737108104 -3600 # Node ID 345e592792fdc79af3c8f53f1bad44973dcbc991 # Parent ea0c7189b15b56e6f76fe4bfba67180d85766aad misc tuning and clarification; diff -r ea0c7189b15b -r 345e592792fd src/HOL/Import/import_rule.ML --- a/src/HOL/Import/import_rule.ML Fri Jan 17 10:56:10 2025 +0100 +++ b/src/HOL/Import/import_rule.ML Fri Jan 17 11:01:44 2025 +0100 @@ -165,14 +165,13 @@ Thm.instantiate (TVars.make (tvars ~~ map (Thm.global_ctyp_of thy) tfrees), Vars.empty) thm end -fun def' constname rhs thy = +fun def' c rhs thy = let - val rhs = Thm.term_of rhs + val b = Binding.name c val typ = type_of rhs - val constbinding = Binding.name constname - val thy1 = Sign.add_consts [(constbinding, typ, NoSyn)] thy - val eq = Logic.mk_equals (Const (Sign.full_name thy1 constbinding, typ), rhs) - val (thm, thy2) = Global_Theory.add_def (Binding.suffix_name "_hldef" constbinding, eq) thy1 + val thy1 = Sign.add_consts [(b, typ, NoSyn)] thy + val eq = Logic.mk_equals (Const (Sign.full_name thy1 b, typ), rhs) + val (thm, thy2) = Global_Theory.add_def (Binding.suffix_name "_hldef" b, eq) thy1 val def_thm = freezeT thy1 thm in (meta_eq_to_obj_eq def_thm, thy2) @@ -183,15 +182,15 @@ SOME th => th | NONE => error ("constant mapped but no definition: " ^ name) -fun def constname rhs thy = - case Import_Data.get_const_def thy constname of +fun def c rhs thy = + case Import_Data.get_const_def thy c of SOME _ => let - val () = warning ("Const mapped but def provided: " ^ constname) + val () = warning ("Const mapped but def provided: " ^ c) in - (mdef thy constname, thy) + (mdef thy c, thy) end - | NONE => def' constname rhs thy + | NONE => def' c (Thm.term_of rhs) thy fun typedef_hol2hollight nty oty rep abs pred a r = Thm.instantiate' [SOME nty, SOME oty] [SOME rep, SOME abs, SOME pred, SOME a, SOME r]