src/Provers/Arith/cancel_numerals.ML
 changeset 9191 300bd596d696 parent 8799 89e9deef4bcb child 9546 be095014e72f
```     1.1 --- a/src/Provers/Arith/cancel_numerals.ML	Thu Jun 29 12:19:27 2000 +0200
1.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Thu Jun 29 16:50:52 2000 +0200
1.3 @@ -69,7 +69,12 @@
1.4
1.5  (*the simplification procedure*)
1.6  fun proc sg _ t =
1.7 -  let val (t1,t2) = Data.dest_bal t
1.8 +  let (*first freeze any Vars in the term to prevent flex-flex problems*)
1.9 +      val rand_s = gensym"_"
1.10 +      fun mk_inst (var as Var((a,i),T))  =
1.11 +	    (var,  Free((a ^ rand_s ^ string_of_int i), T))
1.12 +      val t' = subst_atomic (map mk_inst (term_vars t)) t
1.13 +      val (t1,t2) = Data.dest_bal t'
1.14        val terms1 = Data.dest_sum t1
1.15        and terms2 = Data.dest_sum t2
1.16        val u = find_common (terms1,terms2)
1.17 @@ -81,22 +86,23 @@
1.18  	    if n1=0 orelse n2=0 then   (*trivial, so do nothing*)
1.19  		raise TERM("cancel_numerals", [])
1.20  	    else Data.prove_conv [Data.norm_tac] sg
1.21 -			(t,
1.22 +			(t',
1.23  			 Data.mk_bal (newshape(n1,terms1'),
1.24  				      newshape(n2,terms2')))
1.25    in
1.26 -
1.27        apsome Data.simplify_meta_eq
1.28         (if n2<=n1 then
1.29  	    Data.prove_conv
1.30  	       [Data.trans_tac reshape, rtac Data.bal_add1 1,
1.31  		Data.numeral_simp_tac] sg
1.32 -	       (t, Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum terms2'))
1.33 +	       (t', Data.mk_bal (newshape(n1-n2,terms1'),
1.34 +				 Data.mk_sum terms2'))
1.35  	else
1.36  	    Data.prove_conv
1.37  	       [Data.trans_tac reshape, rtac Data.bal_add2 1,
1.38  		Data.numeral_simp_tac] sg
1.39 -	       (t, Data.mk_bal (Data.mk_sum terms1', newshape(n2-n1,terms2'))))
1.40 +	       (t', Data.mk_bal (Data.mk_sum terms1',
1.41 +				 newshape(n2-n1,terms2'))))
1.42    end
1.43    handle TERM _ => None
1.44         | TYPE _ => None;   (*Typically (if thy doesn't include Numeral)
```