# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260371365 -3600
# Node ID cc0fac4fd46c592a498e1e2fffd3404ff1369fe3
# Parent  546ba31fbb830151a8b6df68ee36b2a8c82055b4
tuned

diff -r 546ba31fbb83 -r cc0fac4fd46c Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Wed Dec 09 15:59:02 2009 +0100
+++ b/Quot/QuotMain.thy	Wed Dec 09 16:09:25 2009 +0100
@@ -144,9 +144,6 @@
 
 declare [[map "fun" = (fun_map, fun_rel)]]
 
-(* Throws now an exception:              *)
-(* declare [[map "option" = (bla, blu)]] *)
-
 lemmas [quot_thm] = fun_quotient 
 
 lemmas [quot_respect] = quot_rel_rsp
@@ -251,25 +248,25 @@
 section {* Matching of Terms and Types *}
 
 ML {*
-fun matches_typ (ty, ty') =
+fun struct_match_typ (ty, ty') =
   case (ty, ty') of
     (_, TVar _) => true
   | (TFree x, TFree x') => x = x'
   | (Type (s, tys), Type (s', tys')) => 
        s = s' andalso 
        if (length tys = length tys') 
-       then (List.all matches_typ (tys ~~ tys')) 
+       then (List.all struct_match_typ (tys ~~ tys')) 
        else false
   | _ => false
 
-fun matches_term (trm, trm') = 
+fun struct_match_term (trm, trm') = 
    case (trm, trm') of 
      (_, Var _) => true
-   | (Const (s, ty), Const (s', ty')) => s = s' andalso matches_typ (ty, ty')
-   | (Free (x, ty), Free (x', ty')) => x = x' andalso matches_typ (ty, ty')
+   | (Const (s, ty), Const (s', ty')) => s = s' andalso struct_match_typ (ty, ty')
+   | (Free (x, ty), Free (x', ty')) => x = x' andalso struct_match_typ (ty, ty')
    | (Bound i, Bound j) => i = j
-   | (Abs (_, T, t), Abs (_, T', t')) => matches_typ (T, T') andalso matches_term (t, t')
-   | (t $ s, t' $ s') => matches_term (t, t') andalso matches_term (s, s') 
+   | (Abs (_, T, t), Abs (_, T', t')) => struct_match_typ (T, T') andalso struct_match_term (t, t')
+   | (t $ s, t' $ s') => struct_match_term (t, t') andalso struct_match_term (s, s') 
    | _ => false
 *}
 
@@ -412,7 +409,7 @@
              val thy = ProofContext.theory_of lthy
              val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1
            in 
-             if matches_term (rtrm, rtrm') then rtrm else
+             if struct_match_term (rtrm, rtrm') then rtrm else
                let
                  val _ = tracing (Syntax.string_of_term @{context} rtrm);
                  val _ = tracing (Syntax.string_of_term @{context} rtrm');
@@ -505,7 +502,6 @@
   shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
 by (simp add: equivp_reflp)
 
-
 (* Regularize Tactic *)
 
 (* 0. preliminary simplification step according to *)
@@ -1185,9 +1181,8 @@
                     (clean_tac ctxt,          "Cleaning proof failed.")]
 *}
 
-(* methods / interface *)
+section {* methods / interface *}
 ML {*
-(* FIXME: if the argument order changes then this can be just one function *)
 fun mk_method1 tac thm ctxt =
   SIMPLE_METHOD (HEADGOAL (tac ctxt thm))