RecordType: use mk_thy_const instead of mk_const

Closes #260
HOL-Theorem-Prover · Jun 2, 2015 · 70888e0 · 70888e0
1 parent 40f6b6e
commit 70888e0
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/datatype/record/RecordType.sml b/src/datatype/record/RecordType.sml
@@ -178,6 +178,7 @@ fun prove_recordtype_thms (tyinfo, fields) = let
     (access_fn_names, access_defn_terms)
   val accessor_thm =
     save_thm(typename^"_accessors", LIST_CONJ access_defns)
+  fun mk_const(n,ty) = mk_thy_const{Thy=current_theory(), Name = n, Ty = ty}
   val accfn_terms = ListPair.map mk_const (access_fn_names, accfn_types)
 
   (* generate functional update functions *)