# HG changeset patch
# User haftmann
# Date 1330697874 -3600
# Node ID aa9f5c3bcd4c99e641e092852fbb7743a004a3a0
# Parent  3c4e327070e567d72dffceae47a21b2f2b7e0f50
dropped dead code

diff -r 3c4e327070e5 -r aa9f5c3bcd4c src/HOL/Library/reflection.ML
--- a/src/HOL/Library/reflection.ML	Fri Mar 02 19:05:13 2012 +0100
+++ b/src/HOL/Library/reflection.ML	Fri Mar 02 15:17:54 2012 +0100
@@ -27,7 +27,7 @@
 
 fun mk_congeq ctxt fs th =
   let
-   val (f as Const(fN,fT)) = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq
+   val Const (fN, _) = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq
      |> fst |> strip_comb |> fst
    val thy = Proof_Context.theory_of ctxt
    val cert = Thm.cterm_of thy
@@ -36,7 +36,7 @@
    fun add_fterms (t as t1 $ t2) =
        if exists (fn f => Term.could_unify (t |> strip_comb |> fst, f)) fs then insert (op aconv) t
        else add_fterms t1 #> add_fterms t2
-     | add_fterms (t as Abs(xn,xT,t')) =
+     | add_fterms (t as Abs _) =
        if exists_Const (fn (c, _) => c = fN) t then (fn _ => [t]) else (fn _ => [])
      | add_fterms _ = I
    val fterms = add_fterms rhs []
@@ -119,7 +119,7 @@
         val cert = cterm_of thy
         fun tryabsdecomp (s,ctxt) bds =
           (case s of
-             Abs(xn,xT,ta) => (
+             Abs(_, xT, ta) => (
                let
                  val ([xn],ctxt') = Variable.variant_fixes ["x"] ctxt
                  val (xn,ta) = Syntax_Trans.variant_abs (xn,xT,ta)  (* FIXME !? *)
@@ -185,8 +185,8 @@
           let
             val rhs = eq |> prop_of |> HOLogic.dest_Trueprop  |> HOLogic.dest_eq |> snd
             val nths = get_nths rhs []
-            val (vss,ns) = fold_rev (fn (_,(vs,n)) => fn (vss,ns) =>
-                                      (insert (op aconv) vs vss, insert (op aconv) n ns)) nths ([],[])
+            val (vss,_ ) = fold_rev (fn (_, (vs, n)) => fn (vss, ns) =>
+              (insert (op aconv) vs vss, insert (op aconv) n ns)) nths ([], [])
             val (vsns, ctxt') = Variable.variant_fixes (replicate (length vss) "vs") ctxt
             val (xns, ctxt'') = Variable.variant_fixes (replicate (length nths) "x") ctxt'
             val thy = Proof_Context.theory_of ctxt''
@@ -202,21 +202,19 @@
             val subst_ty = map (fn (n,(s,t)) => (certT (TVar (n, s)), certT t))
                                (Vartab.dest tyenv)
             val tml = Vartab.dest tmenv
-            val t's = map (fn xn => snd (the (AList.lookup (op =) tml (xn,0)))) xns (* FIXME : Express with sbst*)
             val (subst_ns, bds) = fold_map
-                (fn (Const _ $ vs $ n, Var (xn0,T)) => fn bds =>
+                (fn (Const _ $ _ $ n, Var (xn0, _)) => fn bds =>
                   let
                     val name = snd (the (AList.lookup (op =) tml xn0))
                     val (idx, bds) = index_of name bds
                   in ((cert n, idx |> (HOLogic.mk_nat #> cert)), bds) end) subst bds
             val subst_vs =
               let
-                fun ty (Const _ $ (vs as Var (vsn,lT)) $ n, Var (xn0,T)) = (certT T, certT (sbsT T))
-                fun h (Const _ $ (vs as Var (vsn,lT)) $ n, Var (xn0,T)) =
+                fun h (Const _ $ (vs as Var (_, lT)) $ _, Var (_, T)) =
                   let
                     val cns = sbst (Const(@{const_name "List.Cons"}, T --> lT --> lT))
                     val lT' = sbsT lT
-                    val (bsT,asT) = the (AList.lookup Type.could_unify bds lT)
+                    val (bsT, _) = the (AList.lookup Type.could_unify bds lT)
                     val vsn = the (AList.lookup (op =) vsns_map vs)
                     val cvs = cert (fold_rev (fn x => fn xs => cns$x$xs) bsT (Free (vsn, lT')))
                   in (cert vs, cvs) end
@@ -251,7 +249,7 @@
         val is_Var = can dest_Var
         fun insteq eq vs =
           let
-            val subst = map (fn (v as Var(n,t)) => (cert v, (the o the) (AList.lookup (op =) vstys t)))
+            val subst = map (fn (v as Var(_, t)) => (cert v, (the o the) (AList.lookup (op =) vstys t)))
                         (filter is_Var vs)
           in Thm.instantiate ([],subst) eq
           end
@@ -272,7 +270,7 @@
     val vars = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd
                   |> strip_comb |> snd |> filter is_listVar
     val cert = cterm_of (Proof_Context.theory_of ctxt)
-    val cvs = map (fn (v as Var(n,t)) => (cert v,
+    val cvs = map (fn (v as Var(_, t)) => (cert v,
                   the (AList.lookup Type.could_unify bds t) |> snd |> HOLogic.mk_list (dest_listT t) |> cert)) vars
     val th' = Drule.instantiate_normalize ([], cvs) th
     val t' = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th'