Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/record.ML
changeset 82630 2bb4a8d0111d
parent 81954 6f2bcdfa9a19 
--- a/src/HOL/Tools/record.ML	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Tools/record.ML	Sun May 18 14:33:01 2025 +0000
@@ -86,7 +86,7 @@
     (({rep_type, Abs_name, ...}, {Rep_inject, Abs_inverse, ... }) : Typedef.info) thy =
   let
     val exists_thm =
-      UNIV_I
+      @{thm UNIV_I}
       |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy (Logic.varifyT_global rep_type))] [];
     val proj_constr = Abs_inverse OF [exists_thm];
     val absT = Type (tyco, map TFree vs);
@@ -103,7 +103,7 @@
     thy
     |> Named_Target.theory_map_result (apsnd o Typedef.transform_info)
         (Typedef.add_typedef overloaded (raw_tyco, vs, NoSyn)
-          (HOLogic.mk_UNIV repT) NONE (fn ctxt' => resolve_tac ctxt' [UNIV_witness] 1))
+          (HOLogic.mk_UNIV repT) NONE (fn ctxt' => resolve_tac ctxt' @{thms UNIV_witness} 1))
     |-> (fn (tyco, info) => get_typedef_info tyco vs info)
   end;
isabelle