src/Provers/ind.ML
changeset 4452 b2ee34200dab
parent 1512 ce37c64244c0
child 14643 130076a81b84
     1.1 --- a/src/Provers/ind.ML	Fri Dec 19 10:31:13 1997 +0100
     1.2 +++ b/src/Provers/ind.ML	Fri Dec 19 10:33:24 1997 +0100
     1.3 @@ -43,7 +43,7 @@
     1.4  fun all_frees_tac (var:string) i thm = 
     1.5      let val tsig = #tsig(Sign.rep_sg(#sign(rep_thm thm)));
     1.6          val frees = add_term_frees tsig (nth_elem(i-1,prems_of thm),[var]);
     1.7 -        val frees' = sort(op>)(frees \ var) @ [var]
     1.8 +        val frees' = sort (rev_order o string_ord) (frees \ var) @ [var]
     1.9      in foldl (qnt_tac i) (all_tac,frees') thm end;
    1.10  
    1.11  fun REPEAT_SIMP_TAC simp_tac n i =