# HG changeset patch
# User wenzelm
# Date 1303933804 -7200
# Node ID 1af81b70cf098bdbd8b74fa7f2db0726b0c92083
# Parent  eef1a23c9077efcc9cda06003e4f5e6fc66d02f3
clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;

diff -r eef1a23c9077 -r 1af81b70cf09 src/HOL/Tools/Function/context_tree.ML
--- a/src/HOL/Tools/Function/context_tree.ML	Wed Apr 27 20:58:40 2011 +0200
+++ b/src/HOL/Tools/Function/context_tree.ML	Wed Apr 27 21:50:04 2011 +0200
@@ -103,10 +103,10 @@
 (* Called on the INSTANTIATED branches of the congruence rule *)
 fun mk_branch ctxt t =
   let
-    val ((fixes, impl), ctxt') = Function_Lib.focus_term t ctxt
+    val ((params, impl), ctxt') = Variable.focus t ctxt
     val (assms, concl) = Logic.strip_horn impl
   in
-    (ctxt', fixes, assms, rhs_of concl)
+    (ctxt', map #2 params, assms, rhs_of concl)
   end
 
 fun find_cong_rule ctxt fvar h ((r,dep)::rs) t =
diff -r eef1a23c9077 -r 1af81b70cf09 src/HOL/Tools/Function/function_lib.ML
--- a/src/HOL/Tools/Function/function_lib.ML	Wed Apr 27 20:58:40 2011 +0200
+++ b/src/HOL/Tools/Function/function_lib.ML	Wed Apr 27 21:50:04 2011 +0200
@@ -9,7 +9,6 @@
 sig
   val plural: string -> string -> 'a list -> string
 
-  val focus_term: term -> Proof.context -> ((string * typ) list * term) * Proof.context
   val dest_all_all: term -> term list * term
 
   val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
@@ -39,19 +38,6 @@
   | plural sg pl _ = pl
 
 
-(*term variant of Variable.focus*)
-fun focus_term t ctxt =
-  let
-    val ps = Term.variant_frees t (Term.strip_all_vars t);   (*as they are printed :-*)
-    val (xs, Ts) = split_list ps;
-    val (xs', ctxt') = Variable.variant_fixes xs ctxt;
-    val ps' = xs' ~~ Ts;
-    val inst = map Free ps'
-    val t' = Term.subst_bounds (rev inst, Term.strip_all_body t);
-    val ctxt'' = ctxt' |> fold Variable.declare_constraints inst;
-  in ((ps', t'), ctxt'') end;
-
-
 (* Removes all quantifiers from a term, replacing bound variables by frees. *)
 fun dest_all_all (t as (Const ("all",_) $ _)) =
   let
diff -r eef1a23c9077 -r 1af81b70cf09 src/HOL/Tools/Function/induction_schema.ML
--- a/src/HOL/Tools/Function/induction_schema.ML	Wed Apr 27 20:58:40 2011 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML	Wed Apr 27 21:50:04 2011 +0200
@@ -55,9 +55,9 @@
 
 fun dest_hhf ctxt t =
   let
-    val ((vars, imp), ctxt') = Function_Lib.focus_term t ctxt
+    val ((params, imp), ctxt') = Variable.focus t ctxt
   in
-    (ctxt', vars, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp)
+    (ctxt', map #2 params, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp)
   end
 
 fun mk_scheme' ctxt cases concl =
diff -r eef1a23c9077 -r 1af81b70cf09 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Wed Apr 27 20:58:40 2011 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Wed Apr 27 21:50:04 2011 +0200
@@ -165,7 +165,7 @@
         "Known modes are " ^ commas_quote (known_modes lthy) ^ "."]);
 
     val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [eqn_raw] lthy;
-    val ((_, plain_eqn), _) = Function_Lib.focus_term eqn lthy;
+    val ((_, plain_eqn), _) = Variable.focus eqn lthy;
 
     val ((f_binding, fT), mixfix) = the_single fixes;
     val fname = Binding.name_of f_binding;
diff -r eef1a23c9077 -r 1af81b70cf09 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Wed Apr 27 20:58:40 2011 +0200
+++ b/src/Pure/Isar/element.ML	Wed Apr 27 21:50:04 2011 +0200
@@ -223,8 +223,8 @@
   let
     val ((ps, prop'), ctxt') = Variable.focus prop ctxt;
     fun fix (x, T) = (Binding.name (Variable.revert_fixed ctxt' x), SOME T);
-    val xs = map (fix o Term.dest_Free o Thm.term_of o #2) ps;
-    val As = Logic.strip_imp_prems (Thm.term_of prop');
+    val xs = map (fix o #2) ps;
+    val As = Logic.strip_imp_prems prop';
   in ((Binding.empty, (xs, As)), ctxt') end;
 
 in
@@ -232,7 +232,6 @@
 fun pretty_statement ctxt kind raw_th =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val cert = Thm.cterm_of thy;
 
     val (th, is_elim) = standard_elim (Raw_Simplifier.norm_hhf raw_th);
     val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body true ctxt);
@@ -250,7 +249,7 @@
     pretty_ctxt ctxt' (Assumes (map (fn t => (Attrib.empty_binding, [(t, [])])) assumes)) @
      (if null cases then pretty_stmt ctxt' (Shows [(Attrib.empty_binding, [(concl, [])])])
       else
-        let val (clauses, ctxt'') = fold_map (obtain o cert) cases ctxt'
+        let val (clauses, ctxt'') = fold_map obtain cases ctxt'
         in pretty_stmt ctxt'' (Obtains clauses) end)
   end |> thm_name kind raw_th;
 
diff -r eef1a23c9077 -r 1af81b70cf09 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Wed Apr 27 20:58:40 2011 +0200
+++ b/src/Pure/Isar/obtain.ML	Wed Apr 27 21:50:04 2011 +0200
@@ -196,7 +196,7 @@
     val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule;
     val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt;
     val obtain_rule = Thm.forall_elim (cert (Logic.varify_global (Free thesis_var))) rule';
-    val ((params, stmt), fix_ctxt) = Variable.focus (Thm.cprem_of obtain_rule 1) ctxt';
+    val ((params, stmt), fix_ctxt) = Variable.focus_cterm (Thm.cprem_of obtain_rule 1) ctxt';
     val (prems, ctxt'') =
       Assumption.add_assms (obtain_export fix_ctxt obtain_rule (map #2 params))
         (Drule.strip_imp_prems stmt) fix_ctxt;
diff -r eef1a23c9077 -r 1af81b70cf09 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Wed Apr 27 20:58:40 2011 +0200
+++ b/src/Pure/goal.ML	Wed Apr 27 21:50:04 2011 +0200
@@ -326,7 +326,7 @@
 
 fun assume_rule_tac ctxt = norm_hhf_tac THEN' CSUBGOAL (fn (goal, i) =>
   let
-    val ((_, goal'), ctxt') = Variable.focus goal ctxt;
+    val ((_, goal'), ctxt') = Variable.focus_cterm goal ctxt;
     val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal';
     val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal'');
     val tacs = Rs |> map (fn R =>
diff -r eef1a23c9077 -r 1af81b70cf09 src/Pure/subgoal.ML
--- a/src/Pure/subgoal.ML	Wed Apr 27 20:58:40 2011 +0200
+++ b/src/Pure/subgoal.ML	Wed Apr 27 21:50:04 2011 +0200
@@ -33,7 +33,7 @@
   let
     val st = Simplifier.norm_hhf_protect raw_st;
     val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
-    val ((params, goal), ctxt2) = Variable.focus (Thm.cprem_of st' i) ctxt1;
+    val ((params, goal), ctxt2) = Variable.focus_cterm (Thm.cprem_of st' i) ctxt1;
 
     val (asms, concl) =
       if do_prems then (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal)
diff -r eef1a23c9077 -r 1af81b70cf09 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Wed Apr 27 20:58:40 2011 +0200
+++ b/src/Pure/variable.ML	Wed Apr 27 21:50:04 2011 +0200
@@ -67,7 +67,8 @@
     (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context
   val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
   val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
-  val focus: cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context
+  val focus: term -> Proof.context -> ((string * (string * typ)) list * term) * Proof.context
+  val focus_cterm: cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context
   val focus_subgoal: int -> thm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context
   val warn_extra_tfrees: Proof.context -> Proof.context -> unit
   val polymorphic_types: Proof.context -> term list -> (indexname * sort) list * term list
@@ -516,23 +517,34 @@
 val trade = gen_trade (import true) export;
 
 
-(* focus on outermost parameters *)
+(* focus on outermost parameters: !!x y z. B *)
+
+fun focus_params t ctxt =
+  let
+    val (xs, Ts) =
+      split_list (Term.variant_frees t (Term.strip_all_vars t));  (*as they are printed :-*)
+    val (xs', ctxt') = variant_fixes xs ctxt;
+    val ps = xs' ~~ Ts;
+    val ctxt'' = ctxt' |> fold (declare_constraints o Free) ps;
+  in ((xs, ps), ctxt'') end;
+
+fun focus t ctxt =
+  let
+    val ((xs, ps), ctxt') = focus_params t ctxt;
+    val t' = Term.subst_bounds (rev (map Free ps), Term.strip_all_body t);
+  in (((xs ~~ ps), t'), ctxt') end;
 
 fun forall_elim_prop t prop =
   Thm.beta_conversion false (Thm.capply (Thm.dest_arg prop) t)
   |> Thm.cprop_of |> Thm.dest_arg;
 
-fun focus goal ctxt =
+fun focus_cterm goal ctxt =
   let
     val cert = Thm.cterm_of (Thm.theory_of_cterm goal);
-    val t = Thm.term_of goal;
-    val ps = Term.variant_frees t (Term.strip_all_vars t);   (*as they are printed :-*)
-    val (xs, Ts) = split_list ps;
-    val (xs', ctxt') = variant_fixes xs ctxt;
-    val ps' = ListPair.map (cert o Free) (xs', Ts);
+    val ((xs, ps), ctxt') = focus_params (Thm.term_of goal) ctxt;
+    val ps' = map (cert o Free) ps;
     val goal' = fold forall_elim_prop ps' goal;
-    val ctxt'' = ctxt' |> fold (declare_constraints o Thm.term_of) ps';
-  in ((xs ~~ ps', goal'), ctxt'') end;
+  in ((xs ~~ ps', goal'), ctxt') end;
 
 fun focus_subgoal i st =
   let
@@ -541,7 +553,7 @@
   in
     fold bind_term no_binds #>
     fold (declare_constraints o Var) all_vars #>
-    focus (Thm.cprem_of st i)
+    focus_cterm (Thm.cprem_of st i)
   end;