eliminated redundant parameters;

--- a/src/Pure/Isar/expression.ML	Wed Sep 30 22:20:58 2009 +0200
+++ b/src/Pure/Isar/expression.ML	Wed Sep 30 22:24:57 2009 +0200
@@ -311,7 +311,7 @@
   | finish_primitive _ close (Defines defs) = close (Defines defs)
   | finish_primitive _ _ (Notes facts) = Notes facts;
 
-fun finish_inst ctxt parms do_close (loc, (prfx, inst)) =
+fun finish_inst ctxt (loc, (prfx, inst)) =
   let
     val thy = ProofContext.theory_of ctxt;
     val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
@@ -323,7 +323,7 @@
 
 fun finish ctxt parms do_close insts elems =
   let
-    val deps = map (finish_inst ctxt parms do_close) insts;
+    val deps = map (finish_inst ctxt) insts;
     val elems' = map (finish_elem ctxt parms do_close) elems;
   in (deps, elems') end;
 

--- a/src/Pure/Isar/theory_target.ML	Wed Sep 30 22:20:58 2009 +0200
+++ b/src/Pure/Isar/theory_target.ML	Wed Sep 30 22:24:57 2009 +0200
@@ -45,7 +45,7 @@
 
 (* pretty *)
 
-fun pretty_thy ctxt target is_locale is_class =
+fun pretty_thy ctxt target is_class =
   let
     val thy = ProofContext.theory_of ctxt;
     val target_name = (if is_class then "class " else "locale ") ^ Locale.extern thy target;
@@ -63,12 +63,12 @@
       (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)]
   end;
 
-fun pretty (Target {target, is_locale, is_class, instantiation, overloading, ...}) ctxt =
+fun pretty (Target {target, is_class, instantiation, overloading, ...}) ctxt =
   Pretty.block [Pretty.str "theory", Pretty.brk 1,
       Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] ::
     (if not (null overloading) then [Overloading.pretty ctxt]
      else if not (null (#1 instantiation)) then [Class_Target.pretty_instantiation ctxt]
-     else pretty_thy ctxt target is_locale is_class);
+     else pretty_thy ctxt target is_class);
 
 
 (* target declarations *)
@@ -260,8 +260,7 @@
 
 (* define *)
 
-fun define (ta as Target {target, is_locale, is_class, ...})
-    kind ((b, mx), ((name, atts), rhs)) lthy =
+fun define ta kind ((b, mx), ((name, atts), rhs)) lthy =
   let
     val thy = ProofContext.theory_of lthy;
     val thy_ctxt = ProofContext.init thy;

--- a/src/Pure/Syntax/syn_ext.ML	Wed Sep 30 22:20:58 2009 +0200
+++ b/src/Pure/Syntax/syn_ext.ML	Wed Sep 30 22:24:57 2009 +0200
@@ -270,9 +270,9 @@
     fun rem_pri (Argument (s, _)) = Argument (s, chain_pri)
       | rem_pri sym = sym;
 
-    fun logify_types copy_prod (a as (Argument (s, p))) =
+    fun logify_types (a as (Argument (s, p))) =
           if s <> "prop" andalso is_logtype s then Argument (logic, p) else a
-      | logify_types _ a = a;
+      | logify_types a = a;
 
 
     val raw_symbs = read_mfix sy handle ERROR msg => err_in_mfix msg mfix;
@@ -305,7 +305,7 @@
       if convert andalso not copy_prod then
        (if lhs = "prop" then sprop else if is_logtype lhs then logic else lhs)
       else lhs;
-    val symbs' = map (logify_types copy_prod) symbs;
+    val symbs' = map logify_types symbs;
     val xprod = XProd (lhs', symbs', const', pri);
 
     val _ = (List.app check_pri pris; check_pri pri; check_blocks symbs');

--- a/src/Pure/defs.ML	Wed Sep 30 22:20:58 2009 +0200
+++ b/src/Pure/defs.ML	Wed Sep 30 22:24:57 2009 +0200
@@ -123,7 +123,7 @@
 fun contained (U as TVar _) (Type (_, Ts)) = exists (fn T => T = U orelse contained U T) Ts
   | contained _ _ = false;
 
-fun acyclic pp defs (c, args) (d, Us) =
+fun acyclic pp (c, args) (d, Us) =
   c <> d orelse
   exists (fn U => exists (contained U) args) Us orelse
   is_none (match_args (args, Us)) orelse
@@ -150,7 +150,7 @@
       if forall (is_none o #1) reds then NONE
       else SOME (fold_rev
         (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []);
-    val _ = forall (acyclic pp defs const) (the_default deps deps');
+    val _ = forall (acyclic pp const) (the_default deps deps');
   in deps' end;
 
 in
@@ -163,8 +163,7 @@
           (args, perhaps (reduction pp defs (c, args)) deps));
       in
         if reducts = reducts' then (changed, defs)
-        else (true, defs |> map_def c (fn (specs, restricts, reducts) =>
-          (specs, restricts, reducts')))
+        else (true, defs |> map_def c (fn (specs, restricts, _) => (specs, restricts, reducts')))
       end;
     fun norm_all defs =
       (case Symtab.fold norm_update defs (false, defs) of
@@ -206,7 +205,7 @@
   let
     val restr =
       if plain_args args orelse
-        (case args of [Type (a, rec_args)] => plain_args rec_args | _ => false)
+        (case args of [Type (_, rec_args)] => plain_args rec_args | _ => false)
       then [] else [(args, name)];
     val spec =
       (serial (), {is_def = is_def, name = name, lhs = args, rhs = deps});

--- a/src/Pure/proofterm.ML	Wed Sep 30 22:20:58 2009 +0200
+++ b/src/Pure/proofterm.ML	Wed Sep 30 22:24:57 2009 +0200
@@ -959,7 +959,7 @@
   if ! proofs = 0 then ((name, dummy), Oracle (name, dummy, NONE))
   else ((name, prop), gen_axm_proof Oracle name prop);
 
-fun shrink_proof thy =
+val shrink_proof =
   let
     fun shrink ls lev (prf as Abst (a, T, body)) =
           let val (b, is, ch, body') = shrink ls (lev+1) body
@@ -1319,7 +1319,7 @@
 
     val proof0 =
       if ! proofs = 2 then
-        #4 (shrink_proof thy [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)))
+        #4 (shrink_proof [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)))
       else MinProof;
     val body0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};