diff -r 05585eee8d74 -r 853fa34047a4 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Tue Jan 31 18:19:29 2006 +0100
+++ b/src/Pure/Isar/local_defs.ML	Tue Jan 31 18:19:30 2006 +0100
@@ -7,9 +7,9 @@
 
 signature LOCAL_DEFS =
 sig
-  val mk_def: ProofContext.context -> (string * term) list -> term list
   val cert_def: ProofContext.context -> term -> string * term
   val abs_def: term -> (string * typ) * term
+  val mk_def: ProofContext.context -> (string * term) list -> term list
   val def_export: ProofContext.export
   val add_def: string * term -> ProofContext.context ->
     ((string * typ) * thm) * ProofContext.context
@@ -17,11 +17,11 @@
   val defn_add: attribute
   val defn_del: attribute
   val meta_rewrite_rule: Context.generic -> thm -> thm
-  val unfold: ProofContext.context -> bool -> thm list -> thm -> thm
-  val unfold_goals: ProofContext.context -> bool -> thm list -> thm -> thm
-  val unfold_tac: ProofContext.context -> bool -> thm list -> tactic
-  val fold: ProofContext.context -> bool -> thm list -> thm -> thm
-  val fold_tac: ProofContext.context -> bool -> thm list -> tactic
+  val unfold: ProofContext.context -> thm list -> thm -> thm
+  val unfold_goals: ProofContext.context -> thm list -> thm -> thm
+  val unfold_tac: ProofContext.context -> thm list -> tactic
+  val fold: ProofContext.context -> thm list -> thm -> thm
+  val fold_tac: ProofContext.context -> thm list -> tactic
   val derived_def: ProofContext.context -> term ->
     ((string * typ) * term) * (ProofContext.context -> term -> thm -> thm)
 end;
@@ -33,13 +33,7 @@
 
 (* prepare defs *)
 
-fun mk_def ctxt args =
-  let
-    val (xs, rhss) = split_list args;
-    val (bind, _) = ProofContext.bind_fixes xs ctxt;
-    val lhss = map (fn (x, rhs) => bind (Free (x, Term.fastype_of rhs))) args;
-  in map Logic.mk_equals (lhss ~~ rhss) end;
-
+(*c x == t[x] to !!x. c x == t[x]*)
 fun cert_def ctxt eq =
   let
     fun err msg = cat_error msg
@@ -54,15 +48,14 @@
     fun check_arg (Bound _) = true
       | check_arg (Free (x, _)) = not (ProofContext.is_fixed ctxt x)
       | check_arg t = (case try Logic.dest_type t of SOME (TFree _) => true | _ => false);
-    fun close_arg (Free (x, T)) t = Term.all T $ Term.absfree (x, T, t)
-      | close_arg (Const ("TYPE", T)) t = Term.all T $ Term.absdummy (T, t)
-      | close_arg _ t = t;
+    fun close_arg (Bound _) t = t
+      | close_arg x t = Term.all (Term.fastype_of x) $ lambda x t;
 
     val extra_frees = Term.fold_aterms (fn v as Free (x, _) =>
       if ProofContext.is_fixed ctxt x orelse member (op aconv) xs v then I
       else insert (op =) x | _ => I) rhs [];
   in
-    if not (forall check_arg xs) orelse has_duplicates (op =) xs then
+    if not (forall check_arg xs) orelse has_duplicates (op aconv) xs then
       err "Arguments of lhs must be distinct free/bound variables"
     else if not (null extra_frees) then
       err ("Extra free variables on rhs: " ^ commas_quote extra_frees)
@@ -71,6 +64,7 @@
     else (c, fold_rev close_arg xs eq)
   end;
 
+(*!!x. c x == t[x] to c == %x. t[x]*)
 fun abs_def eq =
   let
     val body = Term.strip_all_body eq;
@@ -80,6 +74,14 @@
     val eq' = Term.list_abs_free (map Term.dest_Free xs, rhs);
   in (Term.dest_Free f, eq') end;
 
+(*c == t*)
+fun mk_def ctxt args =
+  let
+    val (xs, rhss) = split_list args;
+    val (bind, _) = ProofContext.bind_fixes xs ctxt;
+    val lhss = map (fn (x, rhs) => bind (Free (x, Term.fastype_of rhs))) args;
+  in map Logic.mk_equals (lhss ~~ rhss) end;
+
 
 (* export defs *)
 
@@ -87,6 +89,14 @@
   #1 (Term.strip_comb (#1 (Logic.dest_equals (Term.strip_all_body (Thm.term_of cprop)))))
   |> Thm.cterm_of (Thm.theory_of_cterm cprop);
 
+(*
+  [x]
+  [x == t]
+     :
+    B x
+  --------
+    B t
+*)
 fun def_export _ cprops thm =
   thm
   |> Drule.implies_intr_list cprops
@@ -134,7 +144,7 @@
 val defn_del = Thm.declaration_attribute (Rules.map o Drule.del_rule);
 
 
-(* transform rewrite rules *)
+(* meta rewrite rules *)
 
 val equals_ss =
   MetaSimplifier.theory_context ProtoPure.thy MetaSimplifier.empty_ss
@@ -149,14 +159,16 @@
 fun meta_rewrite_tac ctxt i =
   PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal i) (meta_rewrite (Context.Proof ctxt))));
 
-fun transformed f _ false = f
-  | transformed f ctxt true = f o map (meta_rewrite_rule (Context.Proof ctxt));
+
+(* rewriting with object-level rules *)
+
+fun meta f ctxt = f o map (meta_rewrite_rule (Context.Proof ctxt));
 
-val unfold       = transformed Tactic.rewrite_rule;
-val unfold_goals = transformed Tactic.rewrite_goals_rule;
-val unfold_tac   = transformed Tactic.rewrite_goals_tac;
-val fold         = transformed Tactic.fold_rule;
-val fold_tac     = transformed Tactic.fold_goals_tac;
+val unfold       = meta Tactic.rewrite_rule;
+val unfold_goals = meta Tactic.rewrite_goals_rule;
+val unfold_tac   = meta Tactic.rewrite_goals_tac;
+val fold         = meta Tactic.fold_rule;
+val fold_tac     = meta Tactic.fold_goals_tac;
 
 
 (* derived defs -- potentially within the object-logic *)