# HG changeset patch
# User matichuk <daniel.matichuk@nicta.com.au>
# Date 1452556855 -39600
# Node ID 2405ab06d5b148c6beb45f40b57a588fe6c30782
# Parent  43518f70b4383cf4db873b9372c5e206f54e49d0
remove Eisbach's dependency on HOL

diff -r 43518f70b438 -r 2405ab06d5b1 src/HOL/Eisbach/Eisbach.thy
--- a/src/HOL/Eisbach/Eisbach.thy	Mon Jan 11 15:58:18 2016 +1100
+++ b/src/HOL/Eisbach/Eisbach.thy	Tue Jan 12 11:00:55 2016 +1100
@@ -5,7 +5,7 @@
 *)
 
 theory Eisbach
-imports Main
+imports Pure
 keywords
   "method" :: thy_decl and
   "conclusion"
diff -r 43518f70b438 -r 2405ab06d5b1 src/HOL/Eisbach/match_method.ML
--- a/src/HOL/Eisbach/match_method.ML	Mon Jan 11 15:58:18 2016 +1100
+++ b/src/HOL/Eisbach/match_method.ML	Tue Jan 12 11:00:55 2016 +1100
@@ -122,20 +122,22 @@
             then Syntax.parse_prop ctxt3 term
             else Syntax.parse_term ctxt3 term;
 
-          fun drop_Trueprop_dummy t =
+          fun drop_judgment_dummy t =
             (case t of
-              Const (@{const_name Trueprop}, _) $
+              Const (judgment, _) $
                 (Const (@{syntax_const "_type_constraint_"}, T) $
                   Const (@{const_name Pure.dummy_pattern}, _)) =>
+                if judgment = Object_Logic.judgment_name ctxt then
                     Const (@{syntax_const "_type_constraint_"}, T) $
                       Const (@{const_name Pure.dummy_pattern}, propT)
-            | t1 $ t2 => drop_Trueprop_dummy t1 $ drop_Trueprop_dummy t2
-            | Abs (a, T, b) => Abs (a, T, drop_Trueprop_dummy b)
+                else t
+            | t1 $ t2 => drop_judgment_dummy t1 $ drop_judgment_dummy t2
+            | Abs (a, T, b) => Abs (a, T, drop_judgment_dummy b)
             | _ => t);
 
           val pats =
             map (fn (_, (term, _)) => parse_term (Parse_Tools.the_parse_val term)) ts
-            |> map drop_Trueprop_dummy
+            |> map drop_judgment_dummy
             |> (fn ts => fold_map Term.replace_dummy_patterns ts (Variable.maxidx_of ctxt3 + 1))
             |> fst
             |> Syntax.check_terms ctxt3;