# HG changeset patch
# User wenzelm
# Date 1564837553 -7200
# Node ID b2b44fd1b6ecbfb2290f1f32dca1ec5752a5bde4
# Parent  f0a445c5a82c8a7bbfa33c593617c64e52381cd4
tuned;

diff -r f0a445c5a82c -r b2b44fd1b6ec src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Aug 03 12:58:53 2019 +0200
+++ b/src/Pure/thm.ML	Sat Aug 03 15:05:53 2019 +0200
@@ -2227,14 +2227,6 @@
     val arities' = fold (fn (th, c1) => Symtab.cons_list (t, ((c1, Ss), th))) completions arities;
   in (finished', arities') end;
 
-fun put_arity_completion ((t, Ss, c), th) thy =
-  let val ar = ((c, Ss), (th, Context.theory_name thy)) in
-    thy
-    |> map_arities
-      (Symtab.insert_list (eq_fst op =) (t, ar) #>
-        curry (insert_arity_completions thy t ar) true #> #2)
-  end;
-
 fun complete_arities thy =
   let
     val arities = get_arities thy;
@@ -2272,10 +2264,13 @@
     val th = strip_shyps (transfer thy raw_th);
     val prop = plain_prop_of th;
     val (t, Ss, c) = Logic.dest_arity prop;
+    val ar = ((c, Ss), (th |> unconstrainT |> trim_context, Context.theory_name thy))
   in
     thy
     |> Sign.primitive_arity (t, Ss, [c])
-    |> put_arity_completion ((t, Ss, c), th |> unconstrainT |> trim_context)
+    |> map_arities
+      (Symtab.insert_list (eq_fst op =) (t, ar) #>
+        curry (insert_arity_completions thy t ar) true #> #2)
   end;
 
 end;