removed dead code; fixed typo
authorkrauss
Tue, 30 Mar 2010 15:25:35 +0200
changeset 36043 d149c3886e7e
parent 36042 85efdadee8ae
child 36044 10563d88c0b6
removed dead code; fixed typo
src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Tue Mar 30 15:25:30 2010 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Tue Mar 30 15:25:35 2010 +0200
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Tools/inductive_realizer.ML
     Author:     Stefan Berghofer, TU Muenchen
 
-Porgram extraction from proofs involving inductive predicates:
+Program extraction from proofs involving inductive predicates:
 Realizers for induction and elimination rules.
 *)
 
@@ -64,7 +64,6 @@
 fun dt_of_intrs thy vs nparms intrs =
   let
     val iTs = OldTerm.term_tvars (prop_of (hd intrs));
-    val Tvs = map TVar iTs;
     val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
       (Logic.strip_imp_concl (prop_of (hd intrs))));
     val params = map dest_Var (take nparms ts);