# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1258980374 -3600
# Node ID 87eae6a2e5ff835d51761615ff8727f3c3b6348f
# Parent  5a7024be908317715cbf18085ce69fd6ef7e6ada
New repabs behaves the same way as old one.

diff -r 5a7024be9083 -r 87eae6a2e5ff FSet.thy
--- a/FSet.thy	Mon Nov 23 13:24:12 2009 +0100
+++ b/FSet.thy	Mon Nov 23 13:46:14 2009 +0100
@@ -603,10 +603,9 @@
   |> writeln
 *}
 
-ML {* val ttar = REGULARIZE_trm @{context} (prop_of t_a) (term_of glac) *} 
+ML {* val tta = REGULARIZE_trm @{context} (prop_of t_a) (term_of glac) *} 
 
 ML {* val tt = Syntax.check_term @{context} tta *}
-ML {* val ttr = Syntax.check_term @{context} ttar *}
 
 
 
diff -r 5a7024be9083 -r 87eae6a2e5ff IntEx.thy
--- a/IntEx.thy	Mon Nov 23 13:24:12 2009 +0100
+++ b/IntEx.thy	Mon Nov 23 13:46:14 2009 +0100
@@ -177,10 +177,13 @@
   Abs (x, T, subst_bound (trm, t))
 *}
 
+
 ML {*
 (* bound variables need to be treated properly,  *)
 (* as the type of subterms need to be calculated *)
 
+fun is_lifted_const h gh = is_Const h andalso is_Const gh andalso not (h = gh)
+
 fun inj_REPABS lthy (rtrm, qtrm) =
 let
   val rty = fastype_of rtrm
@@ -206,26 +209,20 @@
              then mk_repabs lthy (rty, qty) res
              else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res))
       end
-    (* TODO: check what happens if head is a constant *)
-  | (_ $ _, _ $ _) => 
+  | _ =>
       let
         val (rhead, rargs) = strip_comb rtrm
         val (qhead, qargs) = strip_comb qtrm
-        val rhead' = inj_REPABS lthy (rhead, qhead)
-        val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs)
-        val result = list_comb (rhead', rargs')
+        (* TODO:  val rhead' = inj_REPABS lthy (rhead, qhead) *)
+        val rhead' = rhead;
+        val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs);
+        val result = list_comb (rhead', rargs');
       in
-        if rty = qty
-        then result
-        else mk_repabs lthy (rty, qty) result
+        if rty = qty then result else
+        if (is_lifted_const rhead qhead) then mk_repabs lthy (rty, qty) result else
+        if ((Term.is_Free rhead) andalso (length rargs' > 0)) then mk_repabs lthy (rty, qty) result else
+        if rargs' = [] then rhead' else result
       end
-  (* TODO: maybe leave result without mk_repabs when head is a constant *)
-  (* TODO: that we do not know how to lift *)
-  | (Const (s, T), Const (s', T')) =>
-       if T = T'
-       then rtrm
-       else mk_repabs lthy (T, T') rtrm
-  | _ => rtrm
 end
 *}