# HG changeset patch
# User wenzelm
# Date 1518803742 -3600
# Node ID 357737ccb138165c478451598c740ba13e9cad85
# Parent  bea024ea14ae8e5fbe3a0ed95d943f1152de2a54
removed unused material;

diff -r bea024ea14ae -r 357737ccb138 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Fri Feb 16 18:29:11 2018 +0100
+++ b/src/Pure/axclass.ML	Fri Feb 16 18:55:42 2018 +0100
@@ -420,7 +420,7 @@
 
     val args = Name.invent_names Name.context Name.aT Ss;
     val T = Type (t, map TFree args);
-    val std_vars = map (fn (a, S) => SOME (Thm.global_ctyp_of thy' (TVar ((a, 0), [])))) args;
+    val std_vars = map (fn (a, _) => SOME (Thm.global_ctyp_of thy' (TVar ((a, 0), [])))) args;
 
     val missing_params = Sign.complete_sort thy' [c]
       |> maps (these o Option.map #params o try (get_info thy'))
@@ -456,7 +456,6 @@
   let
     val ctxt = Proof_Context.init_global thy;
     val arity = Proof_Context.cert_arity ctxt raw_arity;
-    val names = map (prefix arity_prefix) (Logic.name_arities arity);
     val props = Logic.mk_arities arity;
     val ths =
       Goal.prove_common ctxt NONE [] [] props
@@ -598,9 +597,6 @@
     |-> fold (add o Drule.export_without_context o snd)
   end;
 
-fun class_const c =
-  (Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT);
-
 fun class_const_dep c =
   ((Defs.Const, Logic.const_of_class c), [Term.aT []]);