src/HOL/Tools/ATP/recon_order_clauses.ML
changeset 15919 b30a35432f5a
parent 15789 4cb16144c81b
child 16061 8a139c1557bf
     1.1 --- a/src/HOL/Tools/ATP/recon_order_clauses.ML	Tue May 03 10:33:31 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_order_clauses.ML	Tue May 03 14:27:21 2005 +0200
     1.3 @@ -242,7 +242,7 @@
     1.4                      (* resulting thm, clause-strs in spass order, vars *)
     1.5  
     1.6  fun rearrange_clause thm res_strlist allvars = 
     1.7 -                          let val isa_strlist = get_meta_lits thm
     1.8 +                          let val isa_strlist = get_meta_lits thm (* change this to use Jia's code to get same looking thing as isastrlist? *)
     1.9                                val (posns, symlist, not_symlist) = checkorder res_strlist isa_strlist allvars([],[],[])
    1.10                                val symmed = apply_rule sym symlist thm
    1.11                                val not_symmed = apply_rule not_sym not_symlist symmed