From f46df86db9308dde29e0e5f97f54546ea1dc34bf Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 18 Jan 2021 23:49:13 +0000
Subject: Swapped notation for metas (now ?) and holes (now {}), other notation
 and name changes.

---
 spartan/core/rewrite.ML | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'spartan/core/rewrite.ML')

diff --git a/spartan/core/rewrite.ML b/spartan/core/rewrite.ML
index 99c21b5..af70cfc 100644
--- a/spartan/core/rewrite.ML
+++ b/spartan/core/rewrite.ML
@@ -72,13 +72,13 @@ fun mk_hole i T = Var ((holeN, i), T)
 fun is_hole (Var ((name, _), _)) = (name = holeN)
   | is_hole _ = false
 
-fun is_hole_const (Const (\<^const_name>\<open>rewrite_HOLE\<close>, _)) = true
+fun is_hole_const (Const (\<^const_name>\<open>rewrite_hole\<close>, _)) = true
   | is_hole_const _ = false
 
 val hole_syntax =
   let
     (* Modified variant of Term.replace_hole *)
-    fun replace_hole Ts (Const (\<^const_name>\<open>rewrite_HOLE\<close>, T)) i =
+    fun replace_hole Ts (Const (\<^const_name>\<open>rewrite_hole\<close>, T)) i =
           (list_comb (mk_hole i (Ts ---> T), map_range Bound (length Ts)), i + 1)
       | replace_hole Ts (Abs (x, T, t)) i =
           let val (t', i') = replace_hole (T :: Ts) t i
-- 
cgit v1.2.3