locale_const/target_notation: uniform use of Term.aconv_untyped;
target_notation: pass on transformed term formally;
removed obsolete Type.similar_types;
--- a/src/Pure/Isar/proof_context.ML Mon Nov 09 19:42:33 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML Mon Nov 09 20:47:39 2009 +0100
@@ -1032,7 +1032,10 @@
(Local_Syntax.update_modesyntax (theory_of ctxt) add mode (map_filter (const_syntax ctxt) args));
fun target_notation add mode args phi =
- let val args' = filter (fn (t, _) => Type.similar_types (t, Morphism.term phi t)) args;
+ let
+ val args' = args |> map_filter (fn (t, mx) =>
+ let val t' = Morphism.term phi t
+ in if Term.aconv_untyped (t, t') then SOME (t', mx) else NONE end);
in Context.mapping (Sign.notation add mode args') (notation add mode args') end;
end;
--- a/src/Pure/Isar/theory_target.ML Mon Nov 09 19:42:33 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML Mon Nov 09 20:47:39 2009 +0100
@@ -190,9 +190,7 @@
val b' = Morphism.binding phi b;
val rhs' = Morphism.term phi rhs;
val arg = (b', Term.close_schematic_term rhs');
-(* val similar_body = Type.similar_types (rhs, rhs'); *)
- val same_shape = op aconv o pairself (Term.map_types (fn _ => Term.dummyT));
- val similar_body = same_shape (rhs, rhs');
+ val same_shape = Term.aconv_untyped (rhs, rhs');
(* FIXME workaround based on educated guess *)
val prefix' = Binding.prefix_of b';
val class_global =
@@ -200,12 +198,12 @@
not (null prefix') andalso
fst (snd (split_last prefix')) = Class_Target.class_prefix target;
in
- not (is_class andalso (similar_body orelse class_global)) ?
+ not (is_class andalso (same_shape orelse class_global)) ?
(Context.mapping_result
(Sign.add_abbrev PrintMode.internal arg)
(ProofContext.add_abbrev PrintMode.internal arg)
#-> (fn (lhs' as Const (d, _), _) =>
- similar_body ?
+ same_shape ?
(Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
end;
--- a/src/Pure/term.ML Mon Nov 09 19:42:33 2009 +0100
+++ b/src/Pure/term.ML Mon Nov 09 20:47:39 2009 +0100
@@ -146,6 +146,7 @@
val eq_ix: indexname * indexname -> bool
val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
val eq_var: (indexname * typ) * (indexname * typ) -> bool
+ val aconv_untyped: term * term -> bool
val could_unify: term * term -> bool
val strip_abs_eta: int -> term -> (string * typ) list * term
val match_bvars: (term * term) * (string * string) list -> (string * string) list
@@ -524,6 +525,17 @@
| (Abs (_, T1, t1), Abs (_, T2, t2)) => t1 aconv t2 andalso T1 = T2
| (a1, a2) => a1 = a2);
+fun aconv_untyped (tm1, tm2) =
+ pointer_eq (tm1, tm2) orelse
+ (case (tm1, tm2) of
+ (t1 $ u1, t2 $ u2) => aconv_untyped (t1, t2) andalso aconv_untyped (u1, u2)
+ | (Abs (_, _, t1), Abs (_, _, t2)) => aconv_untyped (t1, t2)
+ | (Const (a, _), Const (b, _)) => a = b
+ | (Free (x, _), Free (y, _)) => x = y
+ | (Var (xi, _), Var (yj, _)) => xi = yj
+ | (Bound i, Bound j) => i = j
+ | _ => false);
+
(*A fast unification filter: true unless the two terms cannot be unified.
Terms must be NORMAL. Treats all Vars as distinct. *)
--- a/src/Pure/type.ML Mon Nov 09 19:42:33 2009 +0100
+++ b/src/Pure/type.ML Mon Nov 09 20:47:39 2009 +0100
@@ -42,7 +42,6 @@
(*special treatment of type vars*)
val strip_sorts: typ -> typ
- val similar_types: term * term -> bool
val no_tvars: typ -> typ
val varify: (string * sort) list -> term -> ((string * sort) * indexname) list * term
val freeze_thaw_type: typ -> typ * (typ -> typ)
@@ -236,23 +235,6 @@
| strip_sorts (TVar (xi, _)) = TVar (xi, []);
-(* equivalence up to renaming of atomic types *)
-
-local
-
-fun standard_types t =
- let
- val Ts = fold_types (fold_atyps (insert (op =))) t [];
- val Ts' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length Ts));
- in map_types (map_atyps (perhaps (AList.lookup (op =) (Ts ~~ Ts')))) t end;
-
-in
-
-val similar_types = op aconv o pairself (Term.map_types strip_sorts o standard_types);
-
-end;
-
-
(* no_tvars *)
fun no_tvars T =