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/Datatype/rep_datatype.ML
changeset 56239 17df7145a871
parent 56002 2028467b4df4
child 56245 84fc7dfa3cd4 
--- a/src/HOL/Tools/Datatype/rep_datatype.ML	Fri Mar 21 08:13:23 2014 +0100
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Fri Mar 21 10:45:03 2014 +0100
@@ -226,7 +226,7 @@
 
     val (reccomb_defs, thy2) =
       thy1
-      |> Sign.add_consts_i (map (fn ((name, T), T') =>
+      |> Sign.add_consts (map (fn ((name, T), T') =>
             (Binding.name (Long_Name.base_name name), reccomb_fn_Ts @ [T] ---> T', NoSyn))
             (reccomb_names ~~ recTs ~~ rec_result_Ts))
       |> (Global_Theory.add_defs false o map Thm.no_attributes)
isabelle