src/Pure/morphism.ML
changeset 69062 5eda37c06f42
parent 67698 67caf783b9ee
child 70310 c82f59c47aaf
--- a/src/Pure/morphism.ML	Mon Sep 24 20:24:03 2018 +0200
+++ b/src/Pure/morphism.ML	Mon Sep 24 22:05:25 2018 +0200
@@ -24,6 +24,7 @@
     fact: (thm list -> thm list) list} -> morphism
   val pretty: morphism -> Pretty.T
   val binding: morphism -> binding -> binding
+  val binding_prefix: morphism -> (string * bool) list
   val typ: morphism -> typ -> typ
   val term: morphism -> term -> term
   val fact: morphism -> thm list -> thm list
@@ -88,6 +89,7 @@
 val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty);
 
 fun binding (Morphism {binding, ...}) = apply binding;
+fun binding_prefix morph = Binding.name "x" |> binding morph |> Binding.prefix_of;
 fun typ (Morphism {typ, ...}) = apply typ;
 fun term (Morphism {term, ...}) = apply term;
 fun fact (Morphism {fact, ...}) = apply fact;