# HG changeset patch
# User wenzelm
# Date 1302964153 -7200
# Node ID 5528970ac6f7d0e17e3bc6410b919e46c647b342
# Parent  23f35299094493b974515d57b0d713e2474b3cac
observe firm naming convention ctxt: Proof.context;

diff -r 23f352990944 -r 5528970ac6f7 src/HOL/Tools/Function/context_tree.ML
--- a/src/HOL/Tools/Function/context_tree.ML	Sat Apr 16 16:15:37 2011 +0200
+++ b/src/HOL/Tools/Function/context_tree.ML	Sat Apr 16 16:29:13 2011 +0200
@@ -101,29 +101,31 @@
   map (fn c => c RS eq_reflection) [@{thm "cong"}, @{thm "ext"}]
 
 (* Called on the INSTANTIATED branches of the congruence rule *)
-fun mk_branch ctx t =
+fun mk_branch ctxt t =
   let
-    val ((fixes, impl), ctx') = Function_Lib.focus_term t ctx
+    val ((fixes, impl), ctxt') = Function_Lib.focus_term t ctxt
     val (assms, concl) = Logic.strip_horn impl
   in
-    (ctx', fixes, assms, rhs_of concl)
+    (ctxt', fixes, assms, rhs_of concl)
   end
 
-fun find_cong_rule ctx fvar h ((r,dep)::rs) t =
-  (let
-     val thy = Proof_Context.theory_of ctx
+fun find_cong_rule ctxt fvar h ((r,dep)::rs) t =
+     (let
+        val thy = Proof_Context.theory_of ctxt
 
-     val tt' = Logic.mk_equals (Pattern.rewrite_term thy [(Free fvar, h)] [] t, t)
-     val (c, subs) = (concl_of r, prems_of r)
+        val tt' = Logic.mk_equals (Pattern.rewrite_term thy [(Free fvar, h)] [] t, t)
+        val (c, subs) = (concl_of r, prems_of r)
 
-     val subst = Pattern.match (Proof_Context.theory_of ctx) (c, tt') (Vartab.empty, Vartab.empty)
-     val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_term subst) subs
-     val inst = map (fn v =>
-       (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v)))) (Term.add_vars c [])
-   in
-     (cterm_instantiate inst r, dep, branches)
-   end
-   handle Pattern.MATCH => find_cong_rule ctx fvar h rs t)
+        val subst =
+          Pattern.match (Proof_Context.theory_of ctxt) (c, tt') (Vartab.empty, Vartab.empty)
+        val branches = map (mk_branch ctxt o Envir.beta_norm o Envir.subst_term subst) subs
+        val inst = map (fn v =>
+            (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v))))
+          (Term.add_vars c [])
+      in
+         (cterm_instantiate inst r, dep, branches)
+      end
+      handle Pattern.MATCH => find_cong_rule ctxt fvar h rs t)
   | find_cong_rule _ _ _ [] _ = raise General.Fail "No cong rule found!"
 
 
@@ -137,18 +139,18 @@
     fun matchcall (a $ b) = if a = Free fvar then SOME b else NONE
       | matchcall _ = NONE
 
-    fun mk_tree' ctx t =
+    fun mk_tree' ctxt t =
       case matchcall t of
-        SOME arg => RCall (t, mk_tree' ctx arg)
+        SOME arg => RCall (t, mk_tree' ctxt arg)
       | NONE =>
         if not (exists_subterm (fn Free v => v = fvar | _ => false) t) then Leaf t
         else
           let
-            val (r, dep, branches) = find_cong_rule ctx fvar h congs_deps t
-            fun subtree (ctx', fixes, assumes, st) =
+            val (r, dep, branches) = find_cong_rule ctxt fvar h congs_deps t
+            fun subtree (ctxt', fixes, assumes, st) =
               ((fixes,
-                map (Thm.assume o cterm_of (Proof_Context.theory_of ctx)) assumes),
-               mk_tree' ctx' st)
+                map (Thm.assume o cterm_of (Proof_Context.theory_of ctxt)) assumes),
+               mk_tree' ctxt' st)
           in
             Cong (r, dep, map subtree branches)
           end
@@ -216,24 +218,24 @@
 
 fun traverse_tree rcOp tr =
   let
-    fun traverse_help ctx (Leaf _) _ x = ([], x)
-      | traverse_help ctx (RCall (t, st)) u x =
-        rcOp ctx t u (traverse_help ctx st u x)
-      | traverse_help ctx (Cong (_, deps, branches)) u x =
-      let
-        fun sub_step lu i x =
+    fun traverse_help ctxt (Leaf _) _ x = ([], x)
+      | traverse_help ctxt (RCall (t, st)) u x =
+          rcOp ctxt t u (traverse_help ctxt st u x)
+      | traverse_help ctxt (Cong (_, deps, branches)) u x =
           let
-            val (ctx', subtree) = nth branches i
-            val used = fold_rev (append o lu) (Int_Graph.imm_succs deps i) u
-            val (subs, x') = traverse_help (compose ctx ctx') subtree used x
-            val exported_subs = map (apfst (compose ctx')) subs (* FIXME: Right order of composition? *)
+            fun sub_step lu i x =
+              let
+                val (ctxt', subtree) = nth branches i
+                val used = fold_rev (append o lu) (Int_Graph.imm_succs deps i) u
+                val (subs, x') = traverse_help (compose ctxt ctxt') subtree used x
+                val exported_subs = map (apfst (compose ctxt')) subs (* FIXME: Right order of composition? *)
+              in
+                (exported_subs, x')
+              end
           in
-            (exported_subs, x')
+            fold_deps deps sub_step x
+            |> apfst flat
           end
-      in
-        fold_deps deps sub_step x
-        |> apfst flat
-      end
   in
     snd o traverse_help ([], []) tr []
   end
diff -r 23f352990944 -r 5528970ac6f7 src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Sat Apr 16 16:15:37 2011 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Sat Apr 16 16:29:13 2011 +0200
@@ -489,7 +489,7 @@
 fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
   let
     val f_def =
-      Abs ("x", domT, Const (@{const_name FunDef.THE_default}, ranT --> (ranT --> boolT) --> ranT) 
+      Abs ("x", domT, Const (@{const_name FunDef.THE_default}, ranT --> (ranT --> boolT) --> ranT)
         $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
       |> Syntax.check_term lthy
   in
@@ -726,7 +726,7 @@
     fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
       let
         val used = (u @ sub)
-          |> map (fn (ctx,thm) => Function_Ctx_Tree.export_thm thy ctx thm)
+          |> map (fn (ctxt, thm) => Function_Ctx_Tree.export_thm thy ctxt thm)
 
         val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs)
           |> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *)
diff -r 23f352990944 -r 5528970ac6f7 src/HOL/Tools/Function/pattern_split.ML
--- a/src/HOL/Tools/Function/pattern_split.ML	Sat Apr 16 16:15:37 2011 +0200
+++ b/src/HOL/Tools/Function/pattern_split.ML	Sat Apr 16 16:29:13 2011 +0200
@@ -18,15 +18,15 @@
 
 open Function_Lib
 
-fun new_var ctx vs T =
+fun new_var ctxt vs T =
   let
-    val [v] = Variable.variant_frees ctx vs [("v", T)]
+    val [v] = Variable.variant_frees ctxt vs [("v", T)]
   in
     (Free v :: vs, Free v)
   end
 
-fun saturate ctx vs t =
-  fold (fn T => fn (vs, t) => new_var ctx vs T |> apsnd (curry op $ t))
+fun saturate ctxt vs t =
+  fold (fn T => fn (vs, t) => new_var ctxt vs T |> apsnd (curry op $ t))
     (binder_types (fastype_of t)) (vs, t)
 
 
@@ -43,77 +43,77 @@
 
 exception DISJ
 
-fun pattern_subtract_subst ctx vs t t' =
+fun pattern_subtract_subst ctxt vs t t' =
   let
     exception DISJ
     fun pattern_subtract_subst_aux vs _ (Free v2) = []
       | pattern_subtract_subst_aux vs (v as (Free (_, T))) t' =
-      let
-        fun foo constr =
           let
-            val (vs', t) = saturate ctx vs constr
-            val substs = pattern_subtract_subst ctx vs' t t'
+            fun foo constr =
+              let
+                val (vs', t) = saturate ctxt vs constr
+                val substs = pattern_subtract_subst ctxt vs' t t'
+              in
+                map (fn (vs, subst) => (vs, (v,t)::subst)) substs
+              end
           in
-            map (fn (vs, subst) => (vs, (v,t)::subst)) substs
+            maps foo (inst_constrs_of (Proof_Context.theory_of ctxt) T)
           end
-      in
-        maps foo (inst_constrs_of (Proof_Context.theory_of ctx) T)
-      end
      | pattern_subtract_subst_aux vs t t' =
-     let
-       val (C, ps) = strip_comb t
-       val (C', qs) = strip_comb t'
-     in
-       if C = C'
-       then flat (map2 (pattern_subtract_subst_aux vs) ps qs)
-       else raise DISJ
-     end
+         let
+           val (C, ps) = strip_comb t
+           val (C', qs) = strip_comb t'
+         in
+           if C = C'
+           then flat (map2 (pattern_subtract_subst_aux vs) ps qs)
+           else raise DISJ
+         end
   in
     pattern_subtract_subst_aux vs t t'
     handle DISJ => [(vs, [])]
   end
 
 (* p - q *)
-fun pattern_subtract ctx eq2 eq1 =
+fun pattern_subtract ctxt eq2 eq1 =
   let
-    val thy = Proof_Context.theory_of ctx
+    val thy = Proof_Context.theory_of ctxt
 
     val (vs, feq1 as (_ $ (_ $ lhs1 $ _))) = dest_all_all eq1
     val (_,  _ $ (_ $ lhs2 $ _)) = dest_all_all eq2
 
-    val substs = pattern_subtract_subst ctx vs lhs1 lhs2
+    val substs = pattern_subtract_subst ctxt vs lhs1 lhs2
 
     fun instantiate (vs', sigma) =
       let
         val t = Pattern.rewrite_term thy sigma [] feq1
       in
-        fold_rev Logic.all (inter (op =) vs' (map Free (frees_in_term ctx t))) t
+        fold_rev Logic.all (inter (op =) vs' (map Free (frees_in_term ctxt t))) t
       end
   in
     map instantiate substs
   end
 
 (* ps - p' *)
-fun pattern_subtract_from_many ctx p'=
-  maps (pattern_subtract ctx p')
+fun pattern_subtract_from_many ctxt p'=
+  maps (pattern_subtract ctxt p')
 
 (* in reverse order *)
-fun pattern_subtract_many ctx ps' =
-  fold_rev (pattern_subtract_from_many ctx) ps'
+fun pattern_subtract_many ctxt ps' =
+  fold_rev (pattern_subtract_from_many ctxt) ps'
 
-fun split_some_equations ctx eqns =
+fun split_some_equations ctxt eqns =
   let
     fun split_aux prev [] = []
       | split_aux prev ((true, eq) :: es) =
-        pattern_subtract_many ctx prev [eq] :: split_aux (eq :: prev) es
+          pattern_subtract_many ctxt prev [eq] :: split_aux (eq :: prev) es
       | split_aux prev ((false, eq) :: es) =
-        [eq] :: split_aux (eq :: prev) es
+          [eq] :: split_aux (eq :: prev) es
   in
     split_aux [] eqns
   end
 
-fun split_all_equations ctx =
-  split_some_equations ctx o map (pair true)
+fun split_all_equations ctxt =
+  split_some_equations ctxt o map (pair true)
 
 
 end