--- a/src/HOL/Import/hol4rews.ML Tue Apr 05 13:07:40 2011 +0200
+++ b/src/HOL/Import/hol4rews.ML Tue Apr 05 14:25:18 2011 +0200
@@ -610,10 +610,10 @@
end
local
- fun handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax "=="}, _],_,_]] = x
- | handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax all}, _],_]] = x
- | handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax "==>"}, _],_,_]] = x
- | handle_meta [x] = Appl[Constant @{const_syntax Trueprop}, x]
+ fun handle_meta [x as Ast.Appl [Ast.Appl [Ast.Constant "_constrain", Ast.Constant @{const_syntax "=="}, _],_,_]] = x
+ | handle_meta [x as Ast.Appl [Ast.Appl [Ast.Constant "_constrain", Ast.Constant @{const_syntax all}, _],_]] = x
+ | handle_meta [x as Ast.Appl [Ast.Appl [Ast.Constant "_constrain", Ast.Constant @{const_syntax "==>"}, _],_,_]] = x
+ | handle_meta [x] = Ast.Appl [Ast.Constant @{const_syntax Trueprop}, x]
| handle_meta _ = error "hol4rews error: Trueprop not applied to single argument"
in
val smarter_trueprop_parsing = [(@{const_syntax Trueprop},handle_meta)]