# HG changeset patch
# User krauss
# Date 1269955535 -7200
# Node ID d149c3886e7e9002b5240ffb6fe1e84cf5ceb6c5
# Parent  85efdadee8aed0de5122baae687bafb2afe9a2d8
removed dead code; fixed typo

diff -r 85efdadee8ae -r d149c3886e7e 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);