src/HOL/Library/LaTeXsugar.thy
changeset 63414 beb987127d0f
parent 63120 629a4c5e953e
child 63935 aa1fe1103ab8
--- a/src/HOL/Library/LaTeXsugar.thy	Fri Jul 08 16:38:31 2016 +0200
+++ b/src/HOL/Library/LaTeXsugar.thy	Fri Jul 08 19:35:31 2016 +0200
@@ -112,5 +112,21 @@
   end;
 \<close>
 
+setup\<open>
+let
+  fun dummy_pats (wrap $ (eq $ lhs $ rhs)) =
+    let
+      val rhs_vars = Term.add_vars rhs [];
+      fun dummy (v as Var (ixn as (_, T))) =
+            if member (op = ) rhs_vars ixn then v else Const (@{const_name DUMMY}, T)
+        | dummy (t $ u) = dummy t $ dummy u
+        | dummy (Abs (n, T, b)) = Abs (n, T, dummy b)
+        | dummy t = t;
+    in wrap $ (eq $ dummy lhs $ rhs) end
+in
+  Term_Style.setup @{binding dummy_pats} (Scan.succeed (K dummy_pats))
+end
+\<close>
+
 end
 (*>*)