# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260046952 -3600
# Node ID d707839bd9173bdff46af036b61122970f79685a
# Parent  d641c32855f0e4dcf639ad9bddeb467cd1b9aca7
simplified inj_repabs_trm

diff -r d641c32855f0 -r d707839bd917 LFex.thy
--- a/LFex.thy	Sat Dec 05 21:50:31 2009 +0100
+++ b/LFex.thy	Sat Dec 05 22:02:32 2009 +0100
@@ -270,6 +270,8 @@
 ML_prf {* PolyML.profiling 1 *}
 ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *}
 *)
+apply(unfold perm_kind_def perm_ty_def perm_trm_def)
+apply(tactic {* clean_tac @{context} 1 *})
 done
 
 (* Does not work:
diff -r d641c32855f0 -r d707839bd917 QuotMain.thy
--- a/QuotMain.thy	Sat Dec 05 21:50:31 2009 +0100
+++ b/QuotMain.thy	Sat Dec 05 22:02:32 2009 +0100
@@ -741,30 +741,23 @@
         then result
         else mk_repabs lthy (rty, qty) result
       end
-  | _ =>
-      let
-        val (qhead, qargs) = strip_comb qtrm
-        val (rhead, rargs) = strip_combn (length qargs) rtrm
-        val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs)
-      in
-        case (rhead, qhead) of
-          (Const (s, T), Const (s', T')) =>
-             if T = T'                    
-             then list_comb (rhead, rargs') 
-             else list_comb (mk_repabs lthy (T, T') rhead, rargs') 
-        | (Free (x, T), Free (x', T')) => 
-             if T = T' 
-             then list_comb (rhead, rargs')
-             else list_comb (mk_repabs lthy (T, T') rhead, rargs')
-        | (Abs _, Abs _) =>
-             list_comb (inj_repabs_trm lthy (rhead, qhead), rargs') 
- 
-        (* FIXME: when there is an (op =), then lhs might have been a term *) 
-        | (_, Const (@{const_name "op ="}, T)) =>
-             list_comb (rhead, rargs')
-        | _ => raise (LIFT_MATCH ("injection: rhead: " ^ (Syntax.string_of_term lthy rhead) 
-                                          ^ " qhead: " ^ (Syntax.string_of_term lthy qhead)))
-      end
+
+  | (t $ s, t' $ s') =>  
+       (inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s'))
+
+  | (Free (x, T), Free (x', T')) => 
+        if T = T' 
+        then rtrm 
+        else mk_repabs lthy (T, T') rtrm
+
+  | (Const (s, T), Const (s', T')) =>
+        if T = T'                    
+        then rtrm
+        else mk_repabs lthy (T, T') rtrm
+  
+  | (_, Const (@{const_name "op ="}, _)) => rtrm
+  
+  | _ => raise (LIFT_MATCH "injection")
 end
 *}