Get cmlPtreeConvProps to parse (so that Holmake --fast gets through)

CakeML · Feb 15, 2017 · c067d59 · c067d59
1 parent d2a43ca
commit c067d59
Showing 1 changed file with 5 additions and 3 deletions.
diff --git a/semantics/proofs/cmlPtreeConversionPropsScript.sml b/semantics/proofs/cmlPtreeConversionPropsScript.sml
@@ -11,9 +11,11 @@ val _ = export_rewrites ["option.OPTION_IGNORE_BIND_def"]
 
 val ptree_head_TOK = Q.store_thm(
   "ptree_head_TOK",
-  `(ptree_head pt = TOK sym ⇔ pt = Lf (TOK sym)) ∧
-    (TOK sym = ptree_head pt ⇔ pt = Lf (TOK sym))`,
-  Cases_on `pt` >> simp[] >> metis_tac[]);
+  `(ptree_head pt = TOK sym ⇔ ?x. pt = Lf (TOK sym,x)) ∧
+    (TOK sym = ptree_head pt ⇔ ?x. pt = Lf (TOK sym,x))`,
+  Cases_on `pt` >> Cases_on `p` >>
+  simp[grammarTheory.ptree_head_def] >>
+  rw [] >> eq_tac >> rw []);
 val _ = export_rewrites ["ptree_head_TOK"]
 
 val start =