merged

--- a/src/Pure/Isar/local_defs.ML	Thu Mar 11 19:06:03 2010 +0100
+++ b/src/Pure/Isar/local_defs.ML	Thu Mar 11 23:47:16 2010 +0100
@@ -17,7 +17,7 @@
   val fixed_abbrev: (binding * mixfix) * term -> Proof.context ->
     (term * term) * Proof.context
   val export: Proof.context -> Proof.context -> thm -> thm list * thm
-  val export_cterm: Proof.context -> Proof.context -> cterm -> cterm * thm
+  val export_cterm: Proof.context -> Proof.context -> cterm -> thm list * cterm
   val trans_terms: Proof.context -> thm list -> thm
   val trans_props: Proof.context -> thm list -> thm
   val print_rules: Proof.context -> unit
@@ -155,8 +155,7 @@
      TERM b as          b xs == b as
 *)
 fun export_cterm inner outer ct =
-  let val (defs, ct') = export inner outer (Drule.mk_term ct) ||> Drule.dest_term
-  in (ct', MetaSimplifier.rewrite true defs ct) end;
+  export inner outer (Drule.mk_term ct) ||> Drule.dest_term;
 
 
 (* basic transitivity reasoning -- modulo beta-eta *)

--- a/src/Pure/Isar/theory_target.ML	Thu Mar 11 19:06:03 2010 +0100
+++ b/src/Pure/Isar/theory_target.ML	Thu Mar 11 23:47:16 2010 +0100
@@ -278,8 +278,11 @@
     val thy_ctxt = ProofContext.init thy;
 
     val name' = Thm.def_binding_optional b name;
-    val (rhs', rhs_conv) =
-      Local_Defs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
+
+    val crhs = Thm.cterm_of thy rhs;
+    val (defs, rhs') = Local_Defs.export_cterm lthy thy_ctxt crhs ||> Thm.term_of;
+    val rhs_conv = MetaSimplifier.rewrite true defs crhs;
+
     val xs = Variable.add_fixed (Local_Theory.target_of lthy) rhs' [];
     val T = Term.fastype_of rhs;
 

--- a/src/Pure/Isar/typedecl.ML	Thu Mar 11 19:06:03 2010 +0100
+++ b/src/Pure/Isar/typedecl.ML	Thu Mar 11 23:47:16 2010 +0100
@@ -39,8 +39,9 @@
         | SOME S => AxClass.axiomatize_arity (name, replicate n S, S)))
     |> Local_Theory.checkpoint
     |> Local_Theory.type_notation true Syntax.mode_default [(T, mx)]
-    |> Local_Theory.type_syntax false
-      (fn _ => Context.mapping (Sign.type_alias b name) (ProofContext.type_alias b name))
+    |> Local_Theory.type_syntax false (fn phi =>
+        let val b' = Morphism.binding phi b
+        in Context.mapping (Sign.type_alias b' name) (ProofContext.type_alias b' name) end)
     |> ProofContext.type_alias b name
     |> Variable.declare_typ T
     |> pair T

--- a/src/Pure/assumption.ML	Thu Mar 11 19:06:03 2010 +0100
+++ b/src/Pure/assumption.ML	Thu Mar 11 23:47:16 2010 +0100
@@ -6,7 +6,7 @@
 
 signature ASSUMPTION =
 sig
-  type export
+  type export = bool -> cterm list -> (thm -> thm) * (term -> term)
   val assume_export: export
   val presume_export: export
   val assume: cterm -> thm

--- a/src/Pure/more_thm.ML	Thu Mar 11 19:06:03 2010 +0100
+++ b/src/Pure/more_thm.ML	Thu Mar 11 23:47:16 2010 +0100
@@ -324,8 +324,7 @@
 
 fun add_axiom (b, prop) thy =
   let
-    val b' = if Binding.is_empty b
-      then Binding.name ("axiom_" ^ serial_string ()) else b;
+    val b' = if Binding.is_empty b then Binding.name ("axiom_" ^ serial_string ()) else b;
     val thy' = thy |> Theory.add_axioms_i [(b', prop)];
     val axm = unvarify (Thm.axiom thy' (Sign.full_name thy' b'));
   in (axm, thy') end;