merged

--- a/src/Pure/Isar/class.ML	Wed Jun 17 23:22:52 2009 +0200
+++ b/src/Pure/Isar/class.ML	Thu Jun 18 00:00:52 2009 +0200
@@ -78,7 +78,7 @@
         val ((_, [thm']), _) = Variable.import_thms true [thm] empty_ctxt;
         val thm'' = Morphism.thm (const_morph $> eq_morph) thm';
         val tac = ALLGOALS (ProofContext.fact_tac [thm'']);
-      in Goal.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
+      in SkipProof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
     val assm_intro = Option.map prove_assm_intro
       (fst (Locale.intros_of thy class));
 
@@ -95,7 +95,7 @@
       (Tactic.match_tac (axclass_intro :: sup_of_classes
          @ loc_axiom_intros @ base_sort_trivs)
            ORELSE' Tactic.assume_tac));
-    val of_class = Goal.prove_global thy [] [] of_class_prop (K tac);
+    val of_class = SkipProof.prove_global thy [] [] of_class_prop (K tac);
 
   in (base_morph, morph, export_morph, axiom, assm_intro, of_class) end;
 
@@ -281,6 +281,7 @@
     |> Expression.add_locale bname Binding.empty supexpr elems
     |> snd |> LocalTheory.exit_global
     |> adjungate_axclass bname class base_sort sups supsort supparams global_syntax
+    ||> Theory.checkpoint
     |-> (fn (param_map, params, assm_axiom) =>
        `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
     #-> (fn (base_morph, morph, export_morph, axiom, assm_intro, of_class) =>

--- a/src/Pure/Isar/class_target.ML	Wed Jun 17 23:22:52 2009 +0200
+++ b/src/Pure/Isar/class_target.ML	Thu Jun 18 00:00:52 2009 +0200
@@ -351,7 +351,7 @@
     val c' = Sign.full_name thy b;
     val rhs' = Pattern.rewrite_term thy unchecks [] rhs;
     val ty' = Term.fastype_of rhs';
-    val rhs'' = map_types ((*Type.strip_sorts o *)Logic.varifyT) rhs';
+    val rhs'' = map_types Logic.varifyT rhs';
   in
     thy
     |> Sign.add_abbrev (#1 prmode) pos (b, rhs'')

--- a/src/Pure/Isar/overloading.ML	Wed Jun 17 23:22:52 2009 +0200
+++ b/src/Pure/Isar/overloading.ML	Thu Jun 18 00:00:52 2009 +0200
@@ -91,12 +91,17 @@
       |> mark_passed)
   end;
 
+fun rewrite_liberal thy unchecks t =
+  case try (Pattern.rewrite_term thy unchecks []) t
+   of NONE => NONE
+    | SOME t' => if t aconv t' then NONE else SOME t';
+
 fun improve_term_uncheck ts ctxt =
   let
     val thy = ProofContext.theory_of ctxt;
     val unchecks = (#unchecks o ImprovableSyntax.get) ctxt;
-    val ts' = map (Pattern.rewrite_term thy unchecks []) ts;
-  in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end;
+    val ts' = map (rewrite_liberal thy unchecks) ts;
+  in if exists is_some ts' then SOME (map2 the_default ts ts', ctxt) else NONE end;
 
 fun set_primary_constraints ctxt =
   let