--- a/src/HOL/SMT.thy Tue Mar 11 11:32:32 2014 +0100
+++ b/src/HOL/SMT.thy Tue Mar 11 15:34:38 2014 +0100
@@ -425,7 +425,6 @@
by auto
-
hide_type (open) pattern
hide_const Pattern fun_app term_true term_false z3div z3mod
hide_const (open) trigger pat nopat weight
--- a/src/HOL/SMT_Examples/SMT_Word_Examples.thy Tue Mar 11 11:32:32 2014 +0100
+++ b/src/HOL/SMT_Examples/SMT_Word_Examples.thy Tue Mar 11 15:34:38 2014 +0100
@@ -5,7 +5,7 @@
header {* Word examples for for SMT binding *}
theory SMT_Word_Examples
-imports Word
+imports "~~/src/HOL/Word/Word"
begin
declare [[smt_oracle = true]]