src/HOL/cladata.ML
changeset 15570 8d8c70b41bab
parent 12355 c8d3c3d09080
child 17876 b9c92f384109
     1.1 --- a/src/HOL/cladata.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/HOL/cladata.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -33,7 +33,7 @@
     1.4  (*prevent substitution on bool*)
     1.5  fun hyp_subst_tac' i thm = if i <= Thm.nprems_of thm andalso
     1.6    Term.exists_Const (fn ("op =", Type (_, [T, _])) => T <> Type ("bool", []) | _ => false)
     1.7 -    (Library.nth_elem (i - 1, Thm.prems_of thm)) then hyp_subst_tac i thm else no_tac thm;
     1.8 +    (List.nth (Thm.prems_of thm, i - 1)) then hyp_subst_tac i thm else no_tac thm;
     1.9  
    1.10  
    1.11