src/HOL/Tools/inductive_realizer.ML

 (*  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.
 *)
 
 signature INDUCTIVE_REALIZER =
 sig

     | (_, vs) => vs) [] (OldTerm.term_vars prop);
 
 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);
     val tname = Binding.name (space_implode "_" (Long_Name.base_name s ^ "T" :: vs));
     fun constr_of_intr intr = (Binding.name (Long_Name.base_name (name_of_thm intr)),