From 6b27aa578257a6f4db9242b413a8008962b7f2e1 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 28 Jul 2020 14:10:34 +0200
Subject: New `assuming` proof command for elaborated assumptions

---
 spartan/core/goals.ML | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/spartan/core/goals.ML b/spartan/core/goals.ML
index 3e2bd09..87ec2b8 100644
--- a/spartan/core/goals.ML
+++ b/spartan/core/goals.ML
@@ -184,7 +184,7 @@ val schematic_theorem_cmd =
   gen_schematic_theorem
     Bundle.includes_cmd
     Attrib.check_src
-    Elaborated_Expression.read_statement
+    Elaborated_Assumption.read_goal_statement
 
 fun theorem spec descr =
   Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr) 
-- 
cgit v1.2.3