dropped dead code
authorhaftmann
Fri Mar 02 15:17:54 2012 +0100 (2012-03-02)
changeset 46763aa9f5c3bcd4c
parent 46760 3c4e327070e5
child 46764 a65e18ceb1e3
dropped dead code
src/HOL/Library/reflection.ML
     1.1 --- a/src/HOL/Library/reflection.ML	Fri Mar 02 19:05:13 2012 +0100
     1.2 +++ b/src/HOL/Library/reflection.ML	Fri Mar 02 15:17:54 2012 +0100
     1.3 @@ -27,7 +27,7 @@
     1.4  
     1.5  fun mk_congeq ctxt fs th =
     1.6    let
     1.7 -   val (f as Const(fN,fT)) = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq
     1.8 +   val Const (fN, _) = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq
     1.9       |> fst |> strip_comb |> fst
    1.10     val thy = Proof_Context.theory_of ctxt
    1.11     val cert = Thm.cterm_of thy
    1.12 @@ -36,7 +36,7 @@
    1.13     fun add_fterms (t as t1 $ t2) =
    1.14         if exists (fn f => Term.could_unify (t |> strip_comb |> fst, f)) fs then insert (op aconv) t
    1.15         else add_fterms t1 #> add_fterms t2
    1.16 -     | add_fterms (t as Abs(xn,xT,t')) =
    1.17 +     | add_fterms (t as Abs _) =
    1.18         if exists_Const (fn (c, _) => c = fN) t then (fn _ => [t]) else (fn _ => [])
    1.19       | add_fterms _ = I
    1.20     val fterms = add_fterms rhs []
    1.21 @@ -119,7 +119,7 @@
    1.22          val cert = cterm_of thy
    1.23          fun tryabsdecomp (s,ctxt) bds =
    1.24            (case s of
    1.25 -             Abs(xn,xT,ta) => (
    1.26 +             Abs(_, xT, ta) => (
    1.27                 let
    1.28                   val ([xn],ctxt') = Variable.variant_fixes ["x"] ctxt
    1.29                   val (xn,ta) = Syntax_Trans.variant_abs (xn,xT,ta)  (* FIXME !? *)
    1.30 @@ -185,8 +185,8 @@
    1.31            let
    1.32              val rhs = eq |> prop_of |> HOLogic.dest_Trueprop  |> HOLogic.dest_eq |> snd
    1.33              val nths = get_nths rhs []
    1.34 -            val (vss,ns) = fold_rev (fn (_,(vs,n)) => fn (vss,ns) =>
    1.35 -                                      (insert (op aconv) vs vss, insert (op aconv) n ns)) nths ([],[])
    1.36 +            val (vss,_ ) = fold_rev (fn (_, (vs, n)) => fn (vss, ns) =>
    1.37 +              (insert (op aconv) vs vss, insert (op aconv) n ns)) nths ([], [])
    1.38              val (vsns, ctxt') = Variable.variant_fixes (replicate (length vss) "vs") ctxt
    1.39              val (xns, ctxt'') = Variable.variant_fixes (replicate (length nths) "x") ctxt'
    1.40              val thy = Proof_Context.theory_of ctxt''
    1.41 @@ -202,21 +202,19 @@
    1.42              val subst_ty = map (fn (n,(s,t)) => (certT (TVar (n, s)), certT t))
    1.43                                 (Vartab.dest tyenv)
    1.44              val tml = Vartab.dest tmenv
    1.45 -            val t's = map (fn xn => snd (the (AList.lookup (op =) tml (xn,0)))) xns (* FIXME : Express with sbst*)
    1.46              val (subst_ns, bds) = fold_map
    1.47 -                (fn (Const _ $ vs $ n, Var (xn0,T)) => fn bds =>
    1.48 +                (fn (Const _ $ _ $ n, Var (xn0, _)) => fn bds =>
    1.49                    let
    1.50                      val name = snd (the (AList.lookup (op =) tml xn0))
    1.51                      val (idx, bds) = index_of name bds
    1.52                    in ((cert n, idx |> (HOLogic.mk_nat #> cert)), bds) end) subst bds
    1.53              val subst_vs =
    1.54                let
    1.55 -                fun ty (Const _ $ (vs as Var (vsn,lT)) $ n, Var (xn0,T)) = (certT T, certT (sbsT T))
    1.56 -                fun h (Const _ $ (vs as Var (vsn,lT)) $ n, Var (xn0,T)) =
    1.57 +                fun h (Const _ $ (vs as Var (_, lT)) $ _, Var (_, T)) =
    1.58                    let
    1.59                      val cns = sbst (Const(@{const_name "List.Cons"}, T --> lT --> lT))
    1.60                      val lT' = sbsT lT
    1.61 -                    val (bsT,asT) = the (AList.lookup Type.could_unify bds lT)
    1.62 +                    val (bsT, _) = the (AList.lookup Type.could_unify bds lT)
    1.63                      val vsn = the (AList.lookup (op =) vsns_map vs)
    1.64                      val cvs = cert (fold_rev (fn x => fn xs => cns$x$xs) bsT (Free (vsn, lT')))
    1.65                    in (cert vs, cvs) end
    1.66 @@ -251,7 +249,7 @@
    1.67          val is_Var = can dest_Var
    1.68          fun insteq eq vs =
    1.69            let
    1.70 -            val subst = map (fn (v as Var(n,t)) => (cert v, (the o the) (AList.lookup (op =) vstys t)))
    1.71 +            val subst = map (fn (v as Var(_, t)) => (cert v, (the o the) (AList.lookup (op =) vstys t)))
    1.72                          (filter is_Var vs)
    1.73            in Thm.instantiate ([],subst) eq
    1.74            end
    1.75 @@ -272,7 +270,7 @@
    1.76      val vars = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd
    1.77                    |> strip_comb |> snd |> filter is_listVar
    1.78      val cert = cterm_of (Proof_Context.theory_of ctxt)
    1.79 -    val cvs = map (fn (v as Var(n,t)) => (cert v,
    1.80 +    val cvs = map (fn (v as Var(_, t)) => (cert v,
    1.81                    the (AList.lookup Type.could_unify bds t) |> snd |> HOLogic.mk_list (dest_listT t) |> cert)) vars
    1.82      val th' = Drule.instantiate_normalize ([], cvs) th
    1.83      val t' = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th'