# HG changeset patch
# User haftmann
# Date 1433177960 -7200
# Node ID 7d64ad9910e26212b4e0074eb4df905109fdf7dc
# Parent  90d0103af55877dc79079de10c6eeb189e456430
explicit argument expansion of uncheck rules;
rewriting of user-space type system must behave similarly to abbreviations

diff -r 90d0103af558 -r 7d64ad9910e2 NEWS
--- a/NEWS	Mon Jun 01 18:59:20 2015 +0200
+++ b/NEWS	Mon Jun 01 18:59:20 2015 +0200
@@ -13,6 +13,17 @@
 (intermediate legacy feature in Isabelle2015).  INCOMPATIBILITY.
 
 
+*** Pure ***
+
+* Abbreviations in type classes now carry proper sort constraint.
+Rare INCOMPATIBILITY in situations where the previous misbehaviour
+has been exploited previously.
+
+* Refinement of user-space type system in type classes: pseudo-local
+operations behave more similar to abbreviations.  Potential
+INCOMPATIBILITY in exotic situations.
+
+
 *** HOL ***
 
 * Discontinued simp_legacy_precond. Potential INCOMPATIBILITY.
diff -r 90d0103af558 -r 7d64ad9910e2 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Mon Jun 01 18:59:20 2015 +0200
+++ b/src/Pure/Isar/class.ML	Mon Jun 01 18:59:20 2015 +0200
@@ -259,9 +259,22 @@
 
 (* class context syntax *)
 
+fun make_rewrite t c_ty =
+  let
+    val (vs, t') = strip_abs t;
+    val vts = map snd vs
+      |> Name.invent_names Name.context Name.uu
+      |> map (fn (v, T) => Var ((v, 0), T));
+  in (betapplys (t, vts), betapplys (Const c_ty, vts)) end;
+
 fun these_unchecks thy =
-  map_filter (fn (c, (_, ((ty, t), input_only))) => if input_only then NONE else SOME (t, Const (c, ty)))
-  o these_operations thy;
+  these_operations thy
+  #> map_filter (fn (c, (_, ((ty, t), input_only))) =>
+    if input_only then NONE else SOME (make_rewrite t (c, ty)));
+
+fun these_unchecks_reversed thy =
+  these_operations thy
+  #> map (fn (c, (_, ((ty, t), _))) => (Const (c, ty), t));
 
 fun redeclare_const thy c =
   let val b = Long_Name.base_name c
@@ -421,7 +434,7 @@
 fun canonical_abbrev_target class phi prmode ((b, mx), rhs) lthy =
   let
     val thy = Proof_Context.theory_of lthy;
-    val preprocess = perhaps (try (Pattern.rewrite_term thy (these_unchecks thy [class]) []));
+    val preprocess = perhaps (try (Pattern.rewrite_term_top thy (these_unchecks thy [class]) []));
     val (global_rhs, (extra_tfrees, (type_params, term_params))) =
       Generic_Target.export_abbrev lthy preprocess rhs;
     val mx' = Generic_Target.check_mixfix_global (b, null term_params) mx;
@@ -443,7 +456,7 @@
     val thy = Proof_Context.theory_of lthy;
     val phi = morphism thy class;
     val rhs_generic =
-      perhaps (try (Pattern.rewrite_term thy (map swap (these_unchecks thy [class])) [])) rhs;
+      perhaps (try (Pattern.rewrite_term_top thy (these_unchecks_reversed thy [class]) [])) rhs;
   in
     lthy
     |> canonical_abbrev_target class phi prmode ((b, mx), rhs)
diff -r 90d0103af558 -r 7d64ad9910e2 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Mon Jun 01 18:59:20 2015 +0200
+++ b/src/Pure/Isar/overloading.ML	Mon Jun 01 18:59:20 2015 +0200
@@ -87,7 +87,7 @@
   end;
 
 fun rewrite_liberal thy unchecks t =
-  (case try (Pattern.rewrite_term thy unchecks []) t of
+  (case try (Pattern.rewrite_term_top thy unchecks []) t of
     NONE => NONE
   | SOME t' => if t aconv t' then NONE else SOME t');